# HG changeset patch # User wenzelm # Date 1362065897 -3600 # Node ID 102a0a0718c59c5c126b4aadff3957dad89312ac # Parent 0ce544fbb509cab33642d61dbc9b8933571d13a8 discontinued obsolete 'axioms' command; diff -r 0ce544fbb509 -r 102a0a0718c5 NEWS --- 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 diff -r 0ce544fbb509 -r 102a0a0718c5 etc/isar-keywords-ZF.el --- 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" diff -r 0ce544fbb509 -r 102a0a0718c5 etc/isar-keywords.el --- 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" diff -r 0ce544fbb509 -r 102a0a0718c5 src/Doc/IsarRef/Spec.thy --- 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 \ theory"} & (axiomatic!) \\ @{command_def "lemmas"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "theorems"} & : & @{text "local_theory \ 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: \"} 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 \ b\<^sub>n"}~@{keyword_def "for"}~@{text "x\<^sub>1 \ x\<^sub>m"} evaluates given facts (with attributes) in the current context, which may be augmented by local variables. diff -r 0ce544fbb509 -r 102a0a0718c5 src/Pure/Isar/isar_syn.ML --- 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) -- diff -r 0ce544fbb509 -r 102a0a0718c5 src/Pure/Isar/specification.ML --- 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 *) diff -r 0ce544fbb509 -r 102a0a0718c5 src/Pure/Pure.thy --- 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