equal
deleted
inserted
replaced
26 HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s)) |
26 HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s)) |
27 end |
27 end |
28 |
28 |
29 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = |
29 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = |
30 let |
30 let |
31 val _ = Theory.requires thy "Nominal2_Base" "nominal logic"; |
31 val _ = Theory.requires thy (Context.theory_name @{theory}) "nominal logic"; |
32 val str = Sign.full_name thy name; |
32 val str = Sign.full_name thy name; |
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; |
78 (** outer syntax **) |
78 (** outer syntax **) |
79 val _ = |
79 val _ = |
80 Outer_Syntax.command @{command_spec "atom_decl"} |
80 Outer_Syntax.command @{command_spec "atom_decl"} |
81 "declaration of a concrete atom type" |
81 "declaration of a concrete atom type" |
82 ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >> |
82 ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >> |
83 (Toplevel.print oo (Toplevel.theory o add_atom_decl))) |
83 (Toplevel.theory o add_atom_decl)) |
84 |
84 |
85 end; |
85 end; |