changeset 49834 | b27bbb021df1 |
parent 48891 | c0eafbd55de3 |
child 54398 | 100c0eaf63d5 |
--- a/src/HOL/Datatype.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Datatype.thy Fri Oct 12 18:58:20 2012 +0200 @@ -14,7 +14,7 @@ definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" -typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" +typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" morphisms Rep_Node Abs_Node unfolding Node_def by auto