equal
deleted
inserted
replaced
19 |
19 |
20 typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" |
20 typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" |
21 morphisms Rep_Node Abs_Node |
21 morphisms Rep_Node Abs_Node |
22 unfolding Node_def by auto |
22 unfolding Node_def by auto |
23 |
23 |
24 text\<open>Datatypes will be represented by sets of type @{text node}\<close> |
24 text\<open>Datatypes will be represented by sets of type \<open>node\<close>\<close> |
25 |
25 |
26 type_synonym 'a item = "('a, unit) node set" |
26 type_synonym 'a item = "('a, unit) node set" |
27 type_synonym ('a, 'b) dtree = "('a, 'b) node set" |
27 type_synonym ('a, 'b) dtree = "('a, 'b) node set" |
28 |
28 |
29 consts |
29 consts |