equal
deleted
inserted
replaced
33 |
33 |
34 (* typedef *) |
34 (* typedef *) |
35 val set = atom_decl_set str; |
35 val set = atom_decl_set str; |
36 val tac = rtac @{thm exists_eq_simple_sort} 1; |
36 val tac = rtac @{thm exists_eq_simple_sort} 1; |
37 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
37 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
38 Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; |
38 Typedef.add_typedef_global (name, [], NoSyn) set NONE tac thy; |
39 |
39 |
40 (* definition of atom and permute *) |
40 (* definition of atom and permute *) |
41 val newT = #abs_type (fst info); |
41 val newT = #abs_type (fst info); |
42 val RepC = Const (Rep_name, newT --> @{typ atom}); |
42 val RepC = Const (Rep_name, newT --> @{typ atom}); |
43 val AbsC = Const (Abs_name, @{typ atom} --> newT); |
43 val AbsC = Const (Abs_name, @{typ atom} --> newT); |