src/Pure/Isar/isar_thy.ML
changeset 7012 ae9dac5af9d1
parent 7002 01a4e15ee253
child 7103 1c44df10a7bc
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Jul 15 17:53:28 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 15 17:54:58 1999 +0200
     1.3 @@ -123,6 +123,7 @@
     1.4    val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.5    val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.6    val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.7 +  val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
     1.8    val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val also_i: (thm list * Comment.interest) option * Comment.text
    1.11 @@ -224,20 +225,20 @@
    1.12    gen_have_thmss (ProofContext.get_thms o Proof.context_of)
    1.13      (Attrib.local_attribute o Proof.theory_of) x;
    1.14  
    1.15 -fun have_thmss_i f ((name, more_atts), th_atts) =
    1.16 +fun gen_have_thmss_i f ((name, more_atts), th_atts) =
    1.17    f name more_atts (map (apfst single) th_atts);
    1.18  
    1.19  fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]);
    1.20  
    1.21  
    1.22  fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs);
    1.23 -fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs);
    1.24 +fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss ((None, []), th_srcs);
    1.25  val have_theorems = #1 oo (global_have_thmss (PureThy.have_thmss o Some) o Comment.ignore);
    1.26 -val have_theorems_i = #1 oo (have_thmss_i (PureThy.have_thmss o Some) o Comment.ignore);
    1.27 +val have_theorems_i = #1 oo (gen_have_thmss_i (PureThy.have_thmss o Some) o Comment.ignore);
    1.28  val have_lemmas = #1 oo (global_have_thmss (have_lemss o Some) o Comment.ignore);
    1.29 -val have_lemmas_i = #1 oo (have_thmss_i (have_lemss o Some) o Comment.ignore);
    1.30 +val have_lemmas_i = #1 oo (gen_have_thmss_i (have_lemss o Some) o Comment.ignore);
    1.31  val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore;
    1.32 -val have_facts_i = ProofHistory.apply o have_thmss_i (Proof.have_thmss []) o Comment.ignore;
    1.33 +val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore;
    1.34  
    1.35  
    1.36  (* forward chaining *)
    1.37 @@ -248,9 +249,9 @@
    1.38    Proof.have_thmss (Proof.the_facts state) name atts ths_atts state;
    1.39  
    1.40  val from_facts = gen_from_facts (local_have_thmss (Proof.have_thmss [])) o Comment.ignore;
    1.41 -val from_facts_i = gen_from_facts (have_thmss_i (Proof.have_thmss [])) o Comment.ignore;
    1.42 +val from_facts_i = gen_from_facts (gen_have_thmss_i (Proof.have_thmss [])) o Comment.ignore;
    1.43  val with_facts = gen_from_facts (local_have_thmss add_thmss) o Comment.ignore;
    1.44 -val with_facts_i = gen_from_facts (have_thmss_i add_thmss) o Comment.ignore;
    1.45 +val with_facts_i = gen_from_facts (gen_have_thmss_i add_thmss) o Comment.ignore;
    1.46  
    1.47  fun chain comment_ignore = ProofHistory.apply Proof.chain;
    1.48  fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain;
    1.49 @@ -383,14 +384,14 @@
    1.50  
    1.51  fun proof''' f = Toplevel.proof' (f o cond_print_calc);
    1.52  
    1.53 -fun get_thmss srcs = Proof.the_facts o local_have_thmss (Proof.have_thmss []) (("", []), srcs); 
    1.54 -fun get_thmss_i thms _ = thms;
    1.55 -
    1.56  fun gen_calc get f (args, _) prt state =
    1.57    f (apsome (fn (srcs, _) => get srcs state) args) prt state;
    1.58  
    1.59  in
    1.60  
    1.61 +fun get_thmss srcs = Proof.the_facts o local_have_thmss (Proof.have_thmss []) (("", []), srcs); 
    1.62 +fun get_thmss_i thms _ = thms;
    1.63 +
    1.64  fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x);
    1.65  fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
    1.66  fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);