# HG changeset patch
# User wenzelm
# Date 911210755 -3600
# Node ID 2bded7137593db4f2ffd6c50bdd13c35929166dc
# Parent  feec44106a8edf6641a1cf24d11ad495b1bdb5d7
add print_theorems;
print_thms: handle attributes;
renamed tac / etac to refine / then_refine;
tuned comments;
load arg: name;

diff -r feec44106a8e -r 2bded7137593 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 16 11:04:35 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 16 11:05:55 1998 +0100
@@ -11,7 +11,6 @@
   - witness: eliminate (!?);
   - result (interactive): print current result (?);
   - check evaluation of transformers (exns!);
-  - print_thm: attributes;
   - 'result' command;
   - '--' (comment) option everywhere;
   - 'chapter', 'section' etc.;
@@ -315,8 +314,9 @@
 
 val stepP = gen_stepP method;
 
-val tacP = stepP true "tac" "unstructured backward proof step, ignoring facts" IsarThy.tac;
-val etacP = stepP true "etac" "unstructured backward proof step, using facts" IsarThy.etac;
+val refineP = stepP true "refine" "unstructured backward proof step, ignoring facts" IsarThy.tac;
+val then_refineP =
+  stepP true "then_refine" "unstructured backward proof step, using facts" IsarThy.then_tac;
 
 
 val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
@@ -377,12 +377,16 @@
   OuterSyntax.parser true "print_syntax" "print inner syntax of theory (verbose!)"
     (Scan.succeed IsarCmd.print_syntax);
 
+val print_theoremsP =
+  OuterSyntax.parser true "print_theorems" "print theorems known in this theory"
+    (Scan.succeed IsarCmd.print_theorems);
+
 val print_attributesP =
-  OuterSyntax.parser true "print_attributes" "print attributes known in theory"
+  OuterSyntax.parser true "print_attributes" "print attributes known in this theory"
     (Scan.succeed IsarCmd.print_attributes);
 
 val print_methodsP =
-  OuterSyntax.parser true "print_methods" "print methods known in theory"
+  OuterSyntax.parser true "print_methods" "print methods known in this theory"
     (Scan.succeed IsarCmd.print_methods);
 
 val print_bindsP =
@@ -395,7 +399,7 @@
 
 val print_thmP =
   OuterSyntax.parser true "print_thm" "print stored theorem(s)"
-    (xname >> IsarCmd.print_thms);
+    (xname -- opt_attribs >> IsarCmd.print_thms);
 
 val print_propP =
   OuterSyntax.parser true "print_prop" "read and print proposition"
@@ -427,7 +431,7 @@
 
 val loadP =
   OuterSyntax.parser true "load" "load theory file"
-    (string >> IsarCmd.load);
+    (name >> IsarCmd.load);
 
 val prP =
   OuterSyntax.parser true "pr" "print current toplevel state"
@@ -476,13 +480,13 @@
   token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
-  beginP, nextP, qedP, qed_withP, kill_proofP, tacP, etacP, proofP,
-  terminal_proofP, trivial_proofP, default_proofP, clear_undoP, undoP,
-  redoP, backP, prevP, upP, topP,
+  beginP, nextP, qedP, qed_withP, kill_proofP, refineP, then_refineP,
+  proofP, terminal_proofP, trivial_proofP, default_proofP,
+  clear_undoP, undoP, redoP, backP, prevP, upP, topP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
-  print_methodsP, print_bindsP, print_lthmsP, print_thmP, print_propP,
-  print_termP, print_typeP,
+  print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
+  print_thmP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];