src/Pure/Isar/isar_thy.ML
changeset 6501 392333eb31cb
parent 6483 3e5d450c2b31
child 6531 8064ed198068
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Apr 23 16:33:03 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 23 16:33:23 1999 +0200
     1.3 @@ -58,6 +58,12 @@
     1.4    val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
     1.5    val have_i: string -> Proof.context attribute list -> term * term list
     1.6      -> ProofHistory.T -> ProofHistory.T
     1.7 +  val thus: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
     1.8 +  val thus_i: string -> Proof.context attribute list -> term * term list
     1.9 +    -> ProofHistory.T -> ProofHistory.T
    1.10 +  val hence: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    1.11 +  val hence_i: string -> Proof.context attribute list -> term * term list
    1.12 +    -> ProofHistory.T -> ProofHistory.T
    1.13    val begin_block: ProofHistory.T -> ProofHistory.T
    1.14    val next_block: ProofHistory.T -> ProofHistory.T
    1.15    val end_block: ProofHistory.T -> ProofHistory.T
    1.16 @@ -181,22 +187,28 @@
    1.17  fun global_statement f name src s thy =
    1.18    ProofHistory.init (f name (map (Attrib.global_attribute thy) src) s thy);
    1.19  
    1.20 -fun local_statement do_open f name src s = ProofHistory.apply_cond_open do_open (fn state =>
    1.21 -  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s state);
    1.22 +fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
    1.23 +
    1.24 +fun local_statement do_open f g name src s = ProofHistory.apply_cond_open do_open (fn state =>
    1.25 +  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
    1.26  
    1.27 -fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
    1.28 -fun local_statement_i do_open f name atts t = ProofHistory.apply_cond_open do_open (f name atts t);
    1.29 +fun local_statement_i do_open f g name atts t =
    1.30 +  ProofHistory.apply_cond_open do_open (f name atts t o g);
    1.31  
    1.32 -val theorem = global_statement Proof.theorem;
    1.33 +val theorem   = global_statement Proof.theorem;
    1.34  val theorem_i = global_statement_i Proof.theorem_i;
    1.35 -val lemma = global_statement Proof.lemma;
    1.36 -val lemma_i = global_statement_i Proof.lemma_i;
    1.37 -val assume = local_statement false Proof.assume;
    1.38 -val assume_i = local_statement_i false Proof.assume_i;
    1.39 -val show = local_statement true Proof.show;
    1.40 -val show_i = local_statement_i true Proof.show_i;
    1.41 -val have = local_statement true Proof.have;
    1.42 -val have_i = local_statement_i true Proof.have_i;
    1.43 +val lemma     = global_statement Proof.lemma;
    1.44 +val lemma_i   = global_statement_i Proof.lemma_i;
    1.45 +val assume    = local_statement false Proof.assume I;
    1.46 +val assume_i  = local_statement_i false Proof.assume_i I;
    1.47 +val show      = local_statement true Proof.show I;
    1.48 +val show_i    = local_statement_i true Proof.show_i I;
    1.49 +val have      = local_statement true Proof.have I;
    1.50 +val have_i    = local_statement_i true Proof.have_i I;
    1.51 +val thus      = local_statement true Proof.show Proof.chain;
    1.52 +val thus_i    = local_statement_i true Proof.show_i Proof.chain;
    1.53 +val hence     = local_statement true Proof.have Proof.chain;
    1.54 +val hence_i   = local_statement_i true Proof.have_i Proof.chain;
    1.55  
    1.56  
    1.57  (* blocks *)