moved theorem kinds from PureThy to Thm;
authorwenzelm
Tue Nov 21 18:07:33 2006 +0100 (2006-11-21)
changeset 21437a3c55b85cf0e
parent 21436 5313a4cc3823
child 21438 90dda96bca98
moved theorem kinds from PureThy to Thm;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_display.ML
src/Pure/drule.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 21 18:07:32 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 21 18:07:33 2006 +0100
     1.3 @@ -432,7 +432,7 @@
     1.4  
     1.5  fun string_of_stmts state args =
     1.6    Proof.get_thmss state args
     1.7 -  |> map (Element.pretty_statement (Proof.context_of state) PureThy.lemmaK)
     1.8 +  |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
     1.9    |> Pretty.chunks2 |> Pretty.string_of;
    1.10  
    1.11  fun string_of_thms state args =
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 21 18:07:32 2006 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 21 18:07:33 2006 +0100
     2.3 @@ -239,10 +239,10 @@
     2.4    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
     2.5  
     2.6  val theoremsP =
     2.7 -  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK);
     2.8 +  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
     2.9  
    2.10  val lemmasP =
    2.11 -  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems PureThy.lemmaK);
    2.12 +  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
    2.13  
    2.14  val declareP =
    2.15    OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
    2.16 @@ -392,9 +392,9 @@
    2.17         Toplevel.local_theory_to_proof loc
    2.18           (Specification.theorem kind NONE (K I) a elems concl))));
    2.19  
    2.20 -val theoremP = gen_theorem PureThy.theoremK;
    2.21 -val lemmaP = gen_theorem PureThy.lemmaK;
    2.22 -val corollaryP = gen_theorem PureThy.corollaryK;
    2.23 +val theoremP = gen_theorem Thm.theoremK;
    2.24 +val lemmaP = gen_theorem Thm.lemmaK;
    2.25 +val corollaryP = gen_theorem Thm.corollaryK;
    2.26  
    2.27  val haveP =
    2.28    OuterSyntax.command "have" "state local goal"
     3.1 --- a/src/Pure/Isar/proof_display.ML	Tue Nov 21 18:07:32 2006 +0100
     3.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Nov 21 18:07:33 2006 +0100
     3.3 @@ -121,7 +121,7 @@
     3.4    | print_results false = K (K ());
     3.5  
     3.6  fun present_results ctxt ((kind, name), res) =
     3.7 -  if kind = "" orelse kind = PureThy.internalK then ()
     3.8 +  if kind = "" orelse kind = Thm.internalK then ()
     3.9    else (print_results true ctxt ((kind, name), res);
    3.10      Context.setmp (SOME (ProofContext.theory_of ctxt))
    3.11        (Present.results kind) (name_results name res));
     4.1 --- a/src/Pure/drule.ML	Tue Nov 21 18:07:32 2006 +0100
     4.2 +++ b/src/Pure/drule.ML	Tue Nov 21 18:07:33 2006 +0100
     4.3 @@ -934,13 +934,13 @@
     4.4    val term_def = unvarify ProtoPure.term_def;
     4.5  in
     4.6    val protect = Thm.capply (cert Logic.protectC);
     4.7 -  val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
     4.8 +  val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
     4.9        (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
    4.10 -  val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard
    4.11 +  val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
    4.12        (Thm.equal_elim prop_def (Thm.assume (protect A)))));
    4.13    val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
    4.14  
    4.15 -  val termI = store_thm "termI" (PureThy.kind_rule PureThy.internalK (standard
    4.16 +  val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard
    4.17        (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
    4.18  end;
    4.19  
     5.1 --- a/src/Pure/thm.ML	Tue Nov 21 18:07:32 2006 +0100
     5.2 +++ b/src/Pure/thm.ML	Tue Nov 21 18:07:33 2006 +0100
     5.3 @@ -70,6 +70,13 @@
     5.4      tpairs: (cterm * cterm) list,
     5.5      prop: cterm}
     5.6    exception THM of string * int * thm list
     5.7 +  val axiomK: string
     5.8 +  val assumptionK: string
     5.9 +  val definitionK: string
    5.10 +  val theoremK: string
    5.11 +  val lemmaK: string
    5.12 +  val corollaryK: string
    5.13 +  val internalK: string
    5.14    type attribute     (* = Context.generic * thm -> Context.generic * thm *)
    5.15    val eq_thm: thm * thm -> bool
    5.16    val eq_thms: thm list * thm list -> bool
    5.17 @@ -427,6 +434,14 @@
    5.18  fun merge_thys2 (th1 as Thm {thy_ref = r1, ...}) (th2 as Thm {thy_ref = r2, ...}) =
    5.19    Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
    5.20  
    5.21 +(*theorem kinds*)
    5.22 +val axiomK = "axiom";
    5.23 +val assumptionK = "assumption";
    5.24 +val definitionK = "definition";
    5.25 +val theoremK = "theorem";
    5.26 +val lemmaK = "lemma";
    5.27 +val corollaryK = "corollary";
    5.28 +val internalK = "internal";
    5.29  
    5.30  (*attributes subsume any kind of rules or context modifiers*)
    5.31  type attribute = Context.generic * thm -> Context.generic * thm;