added thus, hence;
authorwenzelm
Fri Apr 23 16:33:23 1999 +0200 (1999-04-23 ago)
changeset 6501392333eb31cb
parent 6500 68ba555ac59a
child 6502 bc30e13b36a8
added thus, hence;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 23 16:33:03 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 23 16:33:23 1999 +0200
     1.3 @@ -3,14 +3,6 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Isar/Pure outer syntax.
     1.7 -
     1.8 -TODO:
     1.9 -  - '--' (comment) option almost everywhere:
    1.10 -  - add_parsers: warn if command name coincides with other keyword (if
    1.11 -    not already present) (!?);
    1.12 -  - 'result' (interactive): print current result (?);
    1.13 -  - check evaluation of transformers (exns!);
    1.14 -  - 'thms': xthms1 (vs. 'thm' (!?));
    1.15  *)
    1.16  
    1.17  signature ISAR_SYN =
    1.18 @@ -261,6 +253,14 @@
    1.19    OuterSyntax.command "have" "state local goal"
    1.20      (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
    1.21  
    1.22 +val thusP =
    1.23 +  OuterSyntax.command "thus" "abbreviates \"then show\""
    1.24 +    (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
    1.25 +
    1.26 +val henceP =
    1.27 +  OuterSyntax.command "hence" "abbreviates \"then have\""
    1.28 +    (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
    1.29 +
    1.30  
    1.31  (* facts *)
    1.32  
    1.33 @@ -509,8 +509,8 @@
    1.34    print_translationP, typed_print_translationP,
    1.35    print_ast_translationP, token_translationP, oracleP,
    1.36    (*proof commands*)
    1.37 -  theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
    1.38 -  factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
    1.39 +  theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
    1.40 +  thenP, fromP, factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
    1.41    terminal_proofP, immediate_proofP, default_proofP, refineP,
    1.42    then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
    1.43    backP, prevP, upP, topP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Apr 23 16:33:03 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 23 16:33:23 1999 +0200
     2.3 @@ -58,6 +58,12 @@
     2.4    val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
     2.5    val have_i: string -> Proof.context attribute list -> term * term list
     2.6      -> ProofHistory.T -> ProofHistory.T
     2.7 +  val thus: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
     2.8 +  val thus_i: string -> Proof.context attribute list -> term * term list
     2.9 +    -> ProofHistory.T -> ProofHistory.T
    2.10 +  val hence: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    2.11 +  val hence_i: string -> Proof.context attribute list -> term * term list
    2.12 +    -> ProofHistory.T -> ProofHistory.T
    2.13    val begin_block: ProofHistory.T -> ProofHistory.T
    2.14    val next_block: ProofHistory.T -> ProofHistory.T
    2.15    val end_block: ProofHistory.T -> ProofHistory.T
    2.16 @@ -181,22 +187,28 @@
    2.17  fun global_statement f name src s thy =
    2.18    ProofHistory.init (f name (map (Attrib.global_attribute thy) src) s thy);
    2.19  
    2.20 -fun local_statement do_open f name src s = ProofHistory.apply_cond_open do_open (fn state =>
    2.21 -  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s state);
    2.22 +fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
    2.23 +
    2.24 +fun local_statement do_open f g name src s = ProofHistory.apply_cond_open do_open (fn state =>
    2.25 +  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
    2.26  
    2.27 -fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
    2.28 -fun local_statement_i do_open f name atts t = ProofHistory.apply_cond_open do_open (f name atts t);
    2.29 +fun local_statement_i do_open f g name atts t =
    2.30 +  ProofHistory.apply_cond_open do_open (f name atts t o g);
    2.31  
    2.32 -val theorem = global_statement Proof.theorem;
    2.33 +val theorem   = global_statement Proof.theorem;
    2.34  val theorem_i = global_statement_i Proof.theorem_i;
    2.35 -val lemma = global_statement Proof.lemma;
    2.36 -val lemma_i = global_statement_i Proof.lemma_i;
    2.37 -val assume = local_statement false Proof.assume;
    2.38 -val assume_i = local_statement_i false Proof.assume_i;
    2.39 -val show = local_statement true Proof.show;
    2.40 -val show_i = local_statement_i true Proof.show_i;
    2.41 -val have = local_statement true Proof.have;
    2.42 -val have_i = local_statement_i true Proof.have_i;
    2.43 +val lemma     = global_statement Proof.lemma;
    2.44 +val lemma_i   = global_statement_i Proof.lemma_i;
    2.45 +val assume    = local_statement false Proof.assume I;
    2.46 +val assume_i  = local_statement_i false Proof.assume_i I;
    2.47 +val show      = local_statement true Proof.show I;
    2.48 +val show_i    = local_statement_i true Proof.show_i I;
    2.49 +val have      = local_statement true Proof.have I;
    2.50 +val have_i    = local_statement_i true Proof.have_i I;
    2.51 +val thus      = local_statement true Proof.show Proof.chain;
    2.52 +val thus_i    = local_statement_i true Proof.show_i Proof.chain;
    2.53 +val hence     = local_statement true Proof.have Proof.chain;
    2.54 +val hence_i   = local_statement_i true Proof.have_i Proof.chain;
    2.55  
    2.56  
    2.57  (* blocks *)