example.thy revision e29b8f886533643eb2b9a8601606a9f5e40cd237
theory example
imports Datatype
begin
datatype (type4) 'a type1 =
foo |
bar "'a type2"
and (type5) 'a type2 = "a * nat * 'a type1"
and 'a type3 = "nat * 'a type2"
datatype 'a type6 = bar 'a
consts
I :: "nat type1"
axioms
tt : "test --> test"
lemma I: "A --> A"
proof
assume A
show A by fact
qed
end