--- a/src/Pure/Isar/specification.ML Mon Mar 22 15:07:07 2010 +0100
+++ b/src/Pure/Isar/specification.ML Mon Mar 22 19:23:03 2010 +0100
@@ -32,6 +32,8 @@
val axiomatization_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list -> theory ->
(term list * thm list list) * theory
+ val axiom: Attrib.binding * term -> theory -> thm * theory
+ val axiom_cmd: Attrib.binding * string -> theory -> thm * theory
val definition:
(binding * typ option * mixfix) option * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory
@@ -187,6 +189,9 @@
val axiomatization = gen_axioms false check_specification;
val axiomatization_cmd = gen_axioms true read_specification;
+fun axiom (b, ax) = axiomatization [] [(b, [ax])] #>> (hd o hd o snd);
+fun axiom_cmd (b, ax) = axiomatization_cmd [] [(b, [ax])] #>> (hd o hd o snd);
+
(* definition *)