# HG changeset patch
# User wenzelm
# Date 924878003 -7200
# Node ID 392333eb31cba960b900777b29fad1a280a6bb1b
# Parent  68ba555ac59a5a84538944f754c455fc0a832d4a
added thus, hence;

diff -r 68ba555ac59a -r 392333eb31cb src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 23 16:33:03 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 23 16:33:23 1999 +0200
@@ -3,14 +3,6 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Isar/Pure outer syntax.
-
-TODO:
-  - '--' (comment) option almost everywhere:
-  - add_parsers: warn if command name coincides with other keyword (if
-    not already present) (!?);
-  - 'result' (interactive): print current result (?);
-  - check evaluation of transformers (exns!);
-  - 'thms': xthms1 (vs. 'thm' (!?));
 *)
 
 signature ISAR_SYN =
@@ -261,6 +253,14 @@
   OuterSyntax.command "have" "state local goal"
     (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
 
+val thusP =
+  OuterSyntax.command "thus" "abbreviates \"then show\""
+    (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
+
+val henceP =
+  OuterSyntax.command "hence" "abbreviates \"then have\""
+    (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
+
 
 (* facts *)
 
@@ -509,8 +509,8 @@
   print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
-  theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
-  factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
+  theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
+  thenP, fromP, factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
   terminal_proofP, immediate_proofP, default_proofP, refineP,
   then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
   backP, prevP, upP, topP,
diff -r 68ba555ac59a -r 392333eb31cb src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Apr 23 16:33:03 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 23 16:33:23 1999 +0200
@@ -58,6 +58,12 @@
   val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
   val have_i: string -> Proof.context attribute list -> term * term list
     -> ProofHistory.T -> ProofHistory.T
+  val thus: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
+  val thus_i: string -> Proof.context attribute list -> term * term list
+    -> ProofHistory.T -> ProofHistory.T
+  val hence: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
+  val hence_i: string -> Proof.context attribute list -> term * term list
+    -> ProofHistory.T -> ProofHistory.T
   val begin_block: ProofHistory.T -> ProofHistory.T
   val next_block: ProofHistory.T -> ProofHistory.T
   val end_block: ProofHistory.T -> ProofHistory.T
@@ -181,22 +187,28 @@
 fun global_statement f name src s thy =
   ProofHistory.init (f name (map (Attrib.global_attribute thy) src) s thy);
 
-fun local_statement do_open f name src s = ProofHistory.apply_cond_open do_open (fn state =>
-  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s state);
+fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
+
+fun local_statement do_open f g name src s = ProofHistory.apply_cond_open do_open (fn state =>
+  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
 
-fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
-fun local_statement_i do_open f name atts t = ProofHistory.apply_cond_open do_open (f name atts t);
+fun local_statement_i do_open f g name atts t =
+  ProofHistory.apply_cond_open do_open (f name atts t o g);
 
-val theorem = global_statement Proof.theorem;
+val theorem   = global_statement Proof.theorem;
 val theorem_i = global_statement_i Proof.theorem_i;
-val lemma = global_statement Proof.lemma;
-val lemma_i = global_statement_i Proof.lemma_i;
-val assume = local_statement false Proof.assume;
-val assume_i = local_statement_i false Proof.assume_i;
-val show = local_statement true Proof.show;
-val show_i = local_statement_i true Proof.show_i;
-val have = local_statement true Proof.have;
-val have_i = local_statement_i true Proof.have_i;
+val lemma     = global_statement Proof.lemma;
+val lemma_i   = global_statement_i Proof.lemma_i;
+val assume    = local_statement false Proof.assume I;
+val assume_i  = local_statement_i false Proof.assume_i I;
+val show      = local_statement true Proof.show I;
+val show_i    = local_statement_i true Proof.show_i I;
+val have      = local_statement true Proof.have I;
+val have_i    = local_statement_i true Proof.have_i I;
+val thus      = local_statement true Proof.show Proof.chain;
+val thus_i    = local_statement_i true Proof.show_i Proof.chain;
+val hence     = local_statement true Proof.have Proof.chain;
+val hence_i   = local_statement_i true Proof.have_i Proof.chain;
 
 
 (* blocks *)