--- a/NEWS Thu Feb 28 16:19:08 2013 +0100
+++ b/NEWS Thu Feb 28 16:38:17 2013 +0100
@@ -14,6 +14,13 @@
'ML_file' in Isabelle2013. Minor INCOMPATIBILITY.
+*** Pure ***
+
+* Discontinued obsolete 'axioms' command, which has been marked as
+legacy since Isabelle2009-2. INCOMPATIBILITY, use 'axiomatization'
+instead, while observing its uniform scope for polymorphism.
+
+
*** HOL ***
* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
--- a/etc/isar-keywords-ZF.el Thu Feb 28 16:19:08 2013 +0100
+++ b/etc/isar-keywords-ZF.el Thu Feb 28 16:38:17 2013 +0100
@@ -28,7 +28,6 @@
"assume"
"attribute_setup"
"axiomatization"
- "axioms"
"back"
"bundle"
"by"
@@ -349,7 +348,6 @@
"arities"
"attribute_setup"
"axiomatization"
- "axioms"
"bundle"
"class"
"classes"
--- a/etc/isar-keywords.el Thu Feb 28 16:19:08 2013 +0100
+++ b/etc/isar-keywords.el Thu Feb 28 16:38:17 2013 +0100
@@ -30,7 +30,6 @@
"attribute_setup"
"ax_specification"
"axiomatization"
- "axioms"
"back"
"bnf_def"
"boogie_end"
@@ -472,7 +471,6 @@
"atom_decl"
"attribute_setup"
"axiomatization"
- "axioms"
"boogie_end"
"boogie_open"
"bundle"
--- a/src/Doc/IsarRef/Spec.thy Thu Feb 28 16:19:08 2013 +0100
+++ b/src/Doc/IsarRef/Spec.thy Thu Feb 28 16:38:17 2013 +0100
@@ -270,9 +270,8 @@
These specification mechanisms provide a slightly more abstract view
than the underlying primitives of @{command "consts"}, @{command
- "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see
- \secref{sec:axms-thms}). In particular, type-inference is commonly
- available, and result names need not be given.
+ "defs"} (see \secref{sec:consts}), and raw axioms. In particular,
+ type-inference covers the whole specification as usual.
@{rail "
@@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
@@ -387,7 +386,7 @@
\item @{command "declare"}~@{text thms} declares theorems to the
current local theory context. No theorem binding is involved here,
unlike @{command "theorems"} or @{command "lemmas"} (cf.\
- \secref{sec:axms-thms}), so @{command "declare"} only has the effect
+ \secref{sec:theorems}), so @{command "declare"} only has the effect
of applying attributes as included in the theorem specification.
\end{description}
@@ -1212,18 +1211,15 @@
*}
-section {* Axioms and theorems \label{sec:axms-thms} *}
+section {* Naming existing theorems \label{sec:theorems} *}
text {*
\begin{matharray}{rcll}
- @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
@{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
@{rail "
- @@{command axioms} (@{syntax axmdecl} @{syntax prop} +)
- ;
(@@{command lemmas} | @@{command theorems}) @{syntax target}? \\
(@{syntax thmdef}? @{syntax thmrefs} + @'and')
(@'for' (@{syntax vars} + @'and'))?
@@ -1231,15 +1227,6 @@
\begin{description}
- \item @{command "axioms"}~@{text "a: \<phi>"} introduces arbitrary
- statements as axioms of the meta-logic. In fact, axioms are
- ``axiomatic theorems'', and may be referred later just as any other
- theorem.
-
- Axioms are usually only introduced when declaring new logical
- systems. Everyday work is typically done the hard way, with proper
- definitions and proven theorems.
-
\item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}~@{keyword_def
"for"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"} evaluates given facts (with attributes) in
the current context, which may be augmented by local variables.
--- a/src/Pure/Isar/isar_syn.ML Thu Feb 28 16:19:08 2013 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Feb 28 16:38:17 2013 +0100
@@ -169,13 +169,6 @@
(* axioms and definitions *)
-val _ =
- Outer_Syntax.command @{command_spec "axioms"} "state arbitrary propositions (axiomatic!)"
- (Scan.repeat1 Parse_Spec.spec >>
- (fn spec => Toplevel.theory (fn thy =>
- (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
- fold (snd oo Specification.axiom_cmd) spec thy))));
-
val opt_unchecked_overloaded =
Scan.optional (@{keyword "("} |-- Parse.!!!
(((@{keyword "unchecked"} >> K true) --
--- a/src/Pure/Isar/specification.ML Thu Feb 28 16:19:08 2013 +0100
+++ b/src/Pure/Isar/specification.ML Thu Feb 28 16:38:17 2013 +0100
@@ -32,7 +32,6 @@
(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
@@ -193,7 +192,6 @@
val axiomatization_cmd = gen_axioms 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 *)
--- a/src/Pure/Pure.thy Thu Feb 28 16:19:08 2013 +0100
+++ b/src/Pure/Pure.thy Thu Feb 28 16:38:17 2013 +0100
@@ -25,7 +25,7 @@
and "txt" "txt_raw" :: prf_decl % "proof"
and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
"nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
- "translations" "no_translations" "axioms" "defs" "definition"
+ "translations" "no_translations" "defs" "definition"
"abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl