src/Pure/Isar/isar_thy.ML
changeset 6904 4125d6b6d8f9
parent 6890 05732285677e
child 6937 d9e3e2b30bee
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Jul 06 21:06:03 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Jul 06 21:06:51 1999 +0200
     1.3 @@ -271,35 +271,34 @@
     1.4  fun global_statement_i f (name, atts, t) int thy =
     1.5    ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy);
     1.6  
     1.7 -fun local_statement do_open f g (name, src, s) = ProofHistory.apply_cond_open do_open (fn state =>
     1.8 +fun local_statement f g (name, src, s) = ProofHistory.apply (fn state =>
     1.9    f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
    1.10  
    1.11 -fun local_statement_i do_open f g (name, atts, t) =
    1.12 -  ProofHistory.apply_cond_open do_open (f name atts t o g);
    1.13 +fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
    1.14  
    1.15  val theorem   = global_statement Proof.theorem o Comment.ignore;
    1.16  val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
    1.17  val lemma     = global_statement Proof.lemma o Comment.ignore;
    1.18  val lemma_i   = global_statement_i Proof.lemma_i o Comment.ignore;
    1.19 -val assume    = local_statement false (Proof.assume assume_tac) I o Comment.ignore;
    1.20 -val assume_i  = local_statement_i false (Proof.assume_i assume_tac) I o Comment.ignore;
    1.21 -val presume   = local_statement false (Proof.assume (K all_tac)) I o Comment.ignore;
    1.22 -val presume_i = local_statement_i false (Proof.assume_i (K all_tac)) I o Comment.ignore;
    1.23 -val show      = local_statement true Proof.show I o Comment.ignore;
    1.24 -val show_i    = local_statement_i true Proof.show_i I o Comment.ignore;
    1.25 -val have      = local_statement true Proof.have I o Comment.ignore;
    1.26 -val have_i    = local_statement_i true Proof.have_i I o Comment.ignore;
    1.27 -val thus      = local_statement true Proof.show Proof.chain o Comment.ignore;
    1.28 -val thus_i    = local_statement_i true Proof.show_i Proof.chain o Comment.ignore;
    1.29 -val hence     = local_statement true Proof.have Proof.chain o Comment.ignore;
    1.30 -val hence_i   = local_statement_i true Proof.have_i Proof.chain o Comment.ignore;
    1.31 +val assume    = local_statement (Proof.assume assume_tac) I o Comment.ignore;
    1.32 +val assume_i  = local_statement_i (Proof.assume_i assume_tac) I o Comment.ignore;
    1.33 +val presume   = local_statement (Proof.assume (K all_tac)) I o Comment.ignore;
    1.34 +val presume_i = local_statement_i (Proof.assume_i (K all_tac)) I o Comment.ignore;
    1.35 +val show      = local_statement Proof.show I o Comment.ignore;
    1.36 +val show_i    = local_statement_i Proof.show_i I o Comment.ignore;
    1.37 +val have      = local_statement Proof.have I o Comment.ignore;
    1.38 +val have_i    = local_statement_i Proof.have_i I o Comment.ignore;
    1.39 +val thus      = local_statement Proof.show Proof.chain o Comment.ignore;
    1.40 +val thus_i    = local_statement_i Proof.show_i Proof.chain o Comment.ignore;
    1.41 +val hence     = local_statement Proof.have Proof.chain o Comment.ignore;
    1.42 +val hence_i   = local_statement_i Proof.have_i Proof.chain o Comment.ignore;
    1.43  
    1.44  
    1.45  (* blocks *)
    1.46  
    1.47 -val begin_block = ProofHistory.apply_open Proof.begin_block;
    1.48 +val begin_block = ProofHistory.apply Proof.begin_block;
    1.49  val next_block = ProofHistory.apply Proof.next_block;
    1.50 -val end_block = ProofHistory.apply_close Proof.end_block;
    1.51 +val end_block = ProofHistory.apply Proof.end_block;
    1.52  
    1.53  
    1.54  (* backward steps *)
    1.55 @@ -325,14 +324,14 @@
    1.56  (* local endings *)
    1.57  
    1.58  val local_qed =
    1.59 -  proof'' o (ProofHistory.applys_close oo Method.local_qed) o apsome Comment.ignore_interest;
    1.60 +  proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
    1.61  
    1.62  val local_terminal_proof =
    1.63 -  proof'' o (ProofHistory.applys_close oo Method.local_terminal_proof) o Comment.ignore_interest;
    1.64 +  proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o Comment.ignore_interest;
    1.65  
    1.66 -val local_immediate_proof = proof'' (ProofHistory.applys_close o Method.local_immediate_proof);
    1.67 -val local_default_proof = proof'' (ProofHistory.applys_close o Method.local_default_proof);
    1.68 -val local_skip_proof = proof'' (ProofHistory.applys_close o SkipProof.local_skip_proof);
    1.69 +val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
    1.70 +val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
    1.71 +val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
    1.72  
    1.73  
    1.74  (* global endings *)