src/Pure/Isar/isar_thy.ML
changeset 7271 442456b2a8bb
parent 7242 f17f2e8ba0c7
child 7332 60534b9018ae
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Aug 18 20:45:18 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Aug 18 20:45:52 1999 +0200
     1.3 @@ -83,14 +83,14 @@
     1.4      * Comment.text -> bool -> theory -> ProofHistory.T
     1.5    val lemma_i: (bstring * theory attribute list * (term * (term list * term list)))
     1.6      * Comment.text -> bool -> theory -> ProofHistory.T
     1.7 -  val assume: (string * Args.src list * (string * (string list * string list)) list)
     1.8 -    * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.9 -  val assume_i: (string * Proof.context attribute list * (term * (term list * term list)) list)
    1.10 -    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.11 -  val presume: (string * Args.src list * (string * (string list * string list)) list)
    1.12 -    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.13 -  val presume_i: (string * Proof.context attribute list * (term * (term list * term list)) list)
    1.14 -    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.15 +  val assume: ((string * Args.src list * (string * (string list * string list)) list)
    1.16 +    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.17 +  val assume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list)
    1.18 +    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.19 +  val presume: ((string * Args.src list * (string * (string list * string list)) list)
    1.20 +    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.21 +  val presume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list)
    1.22 +    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.23    val local_def: (string * Args.src list * ((string * string option) * (string * string list)))
    1.24      * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.25    val local_def_i: (string * Args.src list * ((string * typ) * (term * term list)))
    1.26 @@ -273,6 +273,8 @@
    1.27  
    1.28  (* statements *)
    1.29  
    1.30 +local
    1.31 +
    1.32  fun global_statement f (name, src, s) int thy =
    1.33    ProofHistory.init (Toplevel.undo_limit int)
    1.34      (f name (map (Attrib.global_attribute thy) src) s thy);
    1.35 @@ -285,14 +287,22 @@
    1.36  
    1.37  fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
    1.38  
    1.39 +fun multi_statement f args = ProofHistory.apply (fn state =>
    1.40 +  f (map (fn (name, src, s) =>
    1.41 +      (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s)) args) state);
    1.42 +
    1.43 +fun multi_statement_i f args = ProofHistory.apply (f args);
    1.44 +
    1.45 +in
    1.46 +
    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 assume      = multi_statement Proof.assume o map Comment.ignore;
    1.56 +val assume_i    = multi_statement_i Proof.assume_i o map Comment.ignore;
    1.57 +val presume     = multi_statement Proof.presume o map Comment.ignore;
    1.58 +val presume_i   = multi_statement_i Proof.presume_i o map Comment.ignore;
    1.59  val local_def   = local_statement LocalDefs.def I o Comment.ignore;
    1.60  val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore;
    1.61  val show        = local_statement (Proof.show Seq.single) I o Comment.ignore;
    1.62 @@ -304,6 +314,8 @@
    1.63  val hence       = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore;
    1.64  val hence_i     = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore;
    1.65  
    1.66 +end;
    1.67 +
    1.68  
    1.69  (* blocks *)
    1.70