diff -r 985c197f2fe9 -r 338c3f8229e4 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat May 15 23:23:45 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat May 15 23:32:15 2010 +0200 @@ -183,7 +183,7 @@ val _ = OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl - (Scan.repeat1 SpecParse.spec >> + (Scan.repeat1 Parse_Spec.spec >> (Toplevel.theory o (IsarCmd.add_axioms o tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead")))); @@ -196,7 +196,7 @@ val _ = OuterSyntax.command "defs" "define constants" Keyword.thy_decl (opt_unchecked_overloaded -- - Scan.repeat1 (SpecParse.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y))) + Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y))) >> (Toplevel.theory o IsarCmd.add_defs)); @@ -208,7 +208,7 @@ --| Scan.option Parse.where_ >> Parse.triple1 || Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2; -val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- Parse.prop); +val old_constdef = Scan.option old_constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop); val structs = Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure") @@ -223,11 +223,11 @@ val _ = OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl - (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args)); + (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args)); val _ = OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl - (opt_mode -- (Scan.option SpecParse.constdecl -- Parse.prop) + (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop) >> (fn (mode, args) => Specification.abbreviation_cmd mode args)); val _ = @@ -245,13 +245,13 @@ val _ = OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" Keyword.thy_decl - (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix) + (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" Keyword.thy_decl - (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix) + (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); @@ -260,14 +260,14 @@ val _ = OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl (Scan.optional Parse.fixes [] -- - Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 SpecParse.specs)) [] + Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) [] >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y))); (* theorems *) fun theorems kind = - SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args); + Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args); val _ = OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK); @@ -277,7 +277,7 @@ val _ = OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl - (Parse.and_list1 SpecParse.xthms1 + (Parse.and_list1 Parse_Spec.xthms1 >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)])); @@ -416,9 +416,9 @@ (* locales *) val locale_val = - SpecParse.locale_expression false -- - Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] || - Scan.repeat1 SpecParse.context_element >> pair ([], []); + Parse_Spec.locale_expression false -- + Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || + Scan.repeat1 Parse_Spec.context_element >> pair ([], []); val _ = OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl @@ -432,15 +432,15 @@ OuterSyntax.command "sublocale" "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal (Parse.xname --| (Parse.$$$ "\\" || Parse.$$$ "<") -- - Parse.!!! (SpecParse.locale_expression false) + Parse.!!! (Parse_Spec.locale_expression false) >> (fn (loc, expr) => Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))); val _ = OuterSyntax.command "interpretation" "prove interpretation of locale expression in theory" Keyword.thy_goal - (Parse.!!! (SpecParse.locale_expression true) -- - Scan.optional (Parse.where_ |-- Parse.and_list1 (SpecParse.opt_thm_name ":" -- Parse.prop)) [] + (Parse.!!! (Parse_Spec.locale_expression true) -- + Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] >> (fn (expr, equations) => Toplevel.print o Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations))); @@ -448,16 +448,16 @@ OuterSyntax.command "interpret" "prove interpretation of locale expression in proof context" (Keyword.tag_proof Keyword.prf_goal) - (Parse.!!! (SpecParse.locale_expression true) + (Parse.!!! (Parse_Spec.locale_expression true) >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr))); (* classes *) val class_val = - SpecParse.class_expr -- - Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] || - Scan.repeat1 SpecParse.context_element >> pair []; + Parse_Spec.class_expr -- + Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || + Scan.repeat1 Parse_Spec.context_element >> pair []; val _ = OuterSyntax.command "class" "define type class" Keyword.thy_decl @@ -514,9 +514,9 @@ (if schematic then "schematic_" ^ kind else kind) ("state " ^ (if schematic then "schematic " ^ kind else kind)) (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal) - (Scan.optional (SpecParse.opt_thm_name ":" --| - Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding -- - SpecParse.general_statement >> (fn (a, (elems, concl)) => + (Scan.optional (Parse_Spec.opt_thm_name ":" --| + Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding -- + Parse_Spec.general_statement >> (fn (a, (elems, concl)) => ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) kind NONE (K I) a elems concl))); @@ -537,27 +537,27 @@ val _ = OuterSyntax.command "have" "state local goal" (Keyword.tag_proof Keyword.prf_goal) - (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); val _ = OuterSyntax.command "hence" "abbreviates \"then have\"" (Keyword.tag_proof Keyword.prf_goal) - (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); val _ = OuterSyntax.command "show" "state local goal, solving current obligation" (Keyword.tag_proof Keyword.prf_asm_goal) - (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); val _ = OuterSyntax.command "thus" "abbreviates \"then show\"" (Keyword.tag_proof Keyword.prf_asm_goal) - (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); (* facts *) -val facts = Parse.and_list1 SpecParse.xthms1; +val facts = Parse.and_list1 Parse_Spec.xthms1; val _ = OuterSyntax.command "then" "forward chaining" @@ -577,7 +577,7 @@ val _ = OuterSyntax.command "note" "define facts" (Keyword.tag_proof Keyword.prf_decl) - (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd))); + (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd))); val _ = OuterSyntax.command "using" "augment goal facts" @@ -600,18 +600,18 @@ val _ = OuterSyntax.command "assume" "assume propositions" (Keyword.tag_proof Keyword.prf_asm) - (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd))); + (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd))); val _ = OuterSyntax.command "presume" "assume propositions, to be established later" (Keyword.tag_proof Keyword.prf_asm) - (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd))); + (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd))); val _ = OuterSyntax.command "def" "local definition" (Keyword.tag_proof Keyword.prf_asm) (Parse.and_list1 - (SpecParse.opt_thm_name ":" -- + (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix) -- ((Parse.$$$ "\\" || Parse.$$$ "==") |-- Parse.!!! Parse.termp))) >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd))); @@ -619,7 +619,7 @@ val _ = OuterSyntax.command "obtain" "generalized existence" (Keyword.tag_proof Keyword.prf_asm_goal) - (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- SpecParse.statement + (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z))); val _ = @@ -636,13 +636,13 @@ val _ = OuterSyntax.command "write" "add concrete syntax for constants / fixed variables" (Keyword.tag_proof Keyword.prf_decl) - (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix) + (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix) >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args))); val case_spec = (Parse.$$$ "(" |-- Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") || - Parse.xname >> rpair []) -- SpecParse.opt_attribs >> Parse.triple1; + Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1; val _ = OuterSyntax.command "case" "invoke local context" @@ -739,7 +739,7 @@ (* calculational proof commands *) val calc_args = - Scan.option (Parse.$$$ "(" |-- Parse.!!! ((SpecParse.xthms1 --| Parse.$$$ ")"))); + Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")"))); val _ = OuterSyntax.command "also" "combine calculation and current facts" @@ -883,7 +883,7 @@ val _ = OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" - Keyword.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); + Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); val _ = OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag @@ -899,20 +899,20 @@ val _ = OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag - (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); + (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); val _ = OuterSyntax.improper_command "thm" "print theorems" Keyword.diag - (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); + (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); val _ = OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag - (opt_modes -- Scan.option SpecParse.xthms1 + (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); val _ = OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag - (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); + (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); val _ = OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag