added local_def(_i);
authorwenzelm
Fri Jul 09 18:47:56 1999 +0200 (1999-07-09 ago)
changeset 69520f7e8d42902b
parent 6951 13399b560e4e
child 6953 b3f6c39aaa2e
added local_def(_i);
removed global_qed_with(_i);
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jul 09 18:47:15 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Jul 09 18:47:56 1999 +0200
     1.3 @@ -88,6 +88,10 @@
     1.4      * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.5    val presume_i: (string * Proof.context attribute list * (term * (term list * term list)) list)
     1.6      * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.7 +  val local_def: (string * Args.src list * ((string * string option) * (string * string list)))
     1.8 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.9 +  val local_def_i: (string * Args.src list * ((string * typ) * (term * term list)))
    1.10 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.11    val show: (string * Args.src list * (string * (string list * string list)))
    1.12      * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.13    val show_i: (string * Proof.context attribute list * (term * (term list * term list)))
    1.14 @@ -112,12 +116,6 @@
    1.15    val proof: Comment.interest * (Method.text * Comment.interest) option
    1.16      -> ProofHistory.T -> ProofHistory.T
    1.17    val kill_proof: ProofHistory.T -> theory
    1.18 -  val global_qed_with: bstring option * Args.src list option
    1.19 -    -> (Method.text * Comment.interest) option
    1.20 -    -> Toplevel.transition -> Toplevel.transition
    1.21 -  val global_qed_with_i: bstring option * theory attribute list option
    1.22 -    -> (Method.text * Comment.interest) option
    1.23 -    -> Toplevel.transition -> Toplevel.transition
    1.24    val qed: (Method.text * Comment.interest) option -> Toplevel.transition -> Toplevel.transition
    1.25    val terminal_proof: (Method.text * Comment.interest) * (Method.text * Comment.interest) option
    1.26      -> Toplevel.transition -> Toplevel.transition
    1.27 @@ -279,22 +277,24 @@
    1.28  
    1.29  fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
    1.30  
    1.31 -val theorem   = global_statement Proof.theorem o Comment.ignore;
    1.32 -val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
    1.33 -val lemma     = global_statement Proof.lemma o Comment.ignore;
    1.34 -val lemma_i   = global_statement_i Proof.lemma_i o Comment.ignore;
    1.35 -val assume    = local_statement Proof.assume I o Comment.ignore;
    1.36 -val assume_i  = local_statement_i Proof.assume_i I o Comment.ignore;
    1.37 -val presume   = local_statement Proof.presume I o Comment.ignore;
    1.38 -val presume_i = local_statement_i Proof.presume_i I o Comment.ignore;
    1.39 -val show      = local_statement Proof.show I o Comment.ignore;
    1.40 -val show_i    = local_statement_i Proof.show_i I o Comment.ignore;
    1.41 -val have      = local_statement Proof.have I o Comment.ignore;
    1.42 -val have_i    = local_statement_i Proof.have_i I o Comment.ignore;
    1.43 -val thus      = local_statement Proof.show Proof.chain o Comment.ignore;
    1.44 -val thus_i    = local_statement_i Proof.show_i Proof.chain o Comment.ignore;
    1.45 -val hence     = local_statement Proof.have Proof.chain o Comment.ignore;
    1.46 -val hence_i   = local_statement_i Proof.have_i Proof.chain o Comment.ignore;
    1.47 +val theorem     = global_statement Proof.theorem o Comment.ignore;
    1.48 +val theorem_i   = global_statement_i Proof.theorem_i o Comment.ignore;
    1.49 +val lemma       = global_statement Proof.lemma o Comment.ignore;
    1.50 +val lemma_i     = global_statement_i Proof.lemma_i o Comment.ignore;
    1.51 +val assume      = local_statement Proof.assume I o Comment.ignore;
    1.52 +val assume_i    = local_statement_i Proof.assume_i I o Comment.ignore;
    1.53 +val presume     = local_statement Proof.presume I o Comment.ignore;
    1.54 +val presume_i   = local_statement_i Proof.presume_i I o Comment.ignore;
    1.55 +val local_def   = local_statement LocalDefs.def I o Comment.ignore;
    1.56 +val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore;
    1.57 +val show        = local_statement Proof.show I o Comment.ignore;
    1.58 +val show_i      = local_statement_i Proof.show_i I o Comment.ignore;
    1.59 +val have        = local_statement Proof.have I o Comment.ignore;
    1.60 +val have_i      = local_statement_i Proof.have_i I o Comment.ignore;
    1.61 +val thus        = local_statement Proof.show Proof.chain o Comment.ignore;
    1.62 +val thus_i      = local_statement_i Proof.show_i Proof.chain o Comment.ignore;
    1.63 +val hence       = local_statement Proof.have Proof.chain o Comment.ignore;
    1.64 +val hence_i     = local_statement_i Proof.have_i Proof.chain o Comment.ignore;
    1.65  
    1.66  
    1.67  (* blocks *)
    1.68 @@ -350,16 +350,7 @@
    1.69      val (thy, res) = finish state;
    1.70    in print_result res; thy end);
    1.71  
    1.72 -fun gen_global_qed_with prep_att (alt_name, raw_atts) meth state =
    1.73 -  let
    1.74 -    val thy = Proof.theory_of state;
    1.75 -    val alt_atts = apsome (map (prep_att thy)) raw_atts;
    1.76 -  in Method.global_qed alt_name alt_atts (apsome Comment.ignore_interest meth) state end;
    1.77 -
    1.78 -val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute;
    1.79 -val global_qed_with_i = global_result oo gen_global_qed_with (K I);
    1.80 -val global_qed = global_qed_with (None, None);
    1.81 -
    1.82 +val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
    1.83  val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
    1.84  val global_immediate_proof = global_result Method.global_immediate_proof;
    1.85  val global_default_proof = global_result Method.global_default_proof;