theory Datatypes imports Main begin datatype Colour = Red | Green | Blue | Yellow | White datatype Result = OK | Error nat | Exception string lemma "OK ~= Error n" apply (simp) done datatype 'a Tree = Node "'a Tree" 'a "'a Tree" | Leaf lemma t: "(Node l n r) ~= Leaf" apply (simp) done datatype 'a NTree = Node "nat => ('a NTree)" | Leaf 'a (* datatype D = C "D => D" *) (* datatype T = C "T=> bool" *) lemma "(10 + (10 :: int)) = 20" apply (simp) done end