equal
deleted
inserted
replaced
42 |
42 |
43 (* typedef *) |
43 (* typedef *) |
44 val set = atom_decl_set str; |
44 val set = atom_decl_set str; |
45 val tac = rtac @{thm exists_eq_simple_sort} 1; |
45 val tac = rtac @{thm exists_eq_simple_sort} 1; |
46 val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) = |
46 val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) = |
47 Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; |
47 Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy; |
48 |
48 |
49 (* definition of atom and permute *) |
49 (* definition of atom and permute *) |
50 val newT = #abs_type info; |
50 val newT = #abs_type info; |
51 val RepC = Const (Rep_name, newT --> atomT); |
51 val RepC = Const (Rep_name, newT --> atomT); |
52 val AbsC = Const (Abs_name, atomT --> newT); |
52 val AbsC = Const (Abs_name, atomT --> newT); |