equal
deleted
inserted
replaced
10 uses |
10 uses |
11 ("Tools/Datatype/datatype.ML") |
11 ("Tools/Datatype/datatype.ML") |
12 ("Tools/inductive_realizer.ML") |
12 ("Tools/inductive_realizer.ML") |
13 ("Tools/Datatype/datatype_realizer.ML") |
13 ("Tools/Datatype/datatype_realizer.ML") |
14 begin |
14 begin |
|
15 |
|
16 subsection {* Prelude: lifting over function space *} |
|
17 |
|
18 type_lifting map_fun |
|
19 by (simp_all add: fun_eq_iff) |
|
20 |
15 |
21 |
16 subsection {* The datatype universe *} |
22 subsection {* The datatype universe *} |
17 |
23 |
18 typedef (Node) |
24 typedef (Node) |
19 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |
25 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" |