# HG changeset patch
# User wenzelm
# Date 1116773475 -7200
# Node ID 77c1171090d966428790c89fc71f02aec4111130
# Parent  43967e1cba7eda3e58cb1b4c43caba48bfd27021
added 'print_simpset';
tuned 'thms_containing';
removed 'print_intros';

diff -r 43967e1cba7e -r 77c1171090d9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun May 22 16:51:14 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun May 22 16:51:15 2005 +0200
@@ -610,6 +610,10 @@
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
 
+val print_simpsetP =
+  OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
+
 val print_rulesP =
   OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
@@ -630,36 +634,25 @@
   OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
 
-val thms_containingP =
-  let
-    (* intro, elim, dest and rewrite are reserved, otherwise it's a pattern *)
-    fun decode "intro" = ProofContext.Intro
-      | decode "elim" = ProofContext.Elim
-      | decode "dest" = ProofContext.Dest
-      | decode "rewrite" = ProofContext.Rewrite
-      | decode x = ProofContext.Pattern x;
-  
-    (* either name:term or term *)
-    val criterion = ((P.term :-- (fn "name" => P.$$$ ":" |-- P.term | 
-                                     _ => Scan.fail)
-                                 ) >> (ProofContext.Name o #2)) ||
-                    (P.term >> decode);
-  in
-    OuterSyntax.improper_command "thms_containing"
-      "print facts meeting specified criteria"
-      K.diag 
-      (* obtain (int option * (bool * string) list) representing
-         a limit and a set of constraints (the bool indicates whether
-         the constraint is inclusive or exclusive) *)
-      (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
-       Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
-        >> (Toplevel.no_timing oo IsarCmd.print_thms_containing))
-  end;
-
 val thm_depsP =
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
     K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
 
+val criterion =
+  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
+  P.reserved "intro" >> K FindTheorems.Intro ||
+  P.reserved "elim" >> K FindTheorems.Elim ||
+  P.reserved "dest" >> K FindTheorems.Dest ||
+  P.reserved "rewrite" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Rewrite ||
+  P.term >> FindTheorems.Pattern;
+
+val find_theoremsP =
+  OuterSyntax.improper_command "thms_containing"  (* FIXME rename to "find_theorems" *)
+    "print theorems meeting specified criteria" K.diag
+    (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
+     Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+      >> (Toplevel.no_timing oo IsarCmd.find_theorems));
+
 val print_bindsP =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
@@ -672,10 +665,6 @@
   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
 
-val print_introsP =
-  OuterSyntax.improper_command "print_intros" "print matching introduction rules" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_intros));
-
 val print_thmsP =
   OuterSyntax.improper_command "thm" "print theorems" K.diag
     (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
@@ -828,16 +817,15 @@
   default_proofP, immediate_proofP, done_proofP, skip_proofP,
   forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
   finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
-  redoP, undos_proofP, undoP, killP, interpretationP, interpretP, instantiateP,
-  (*diagnostic commands*)
-  pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
-  print_syntaxP, print_theoremsP, print_localesP, print_localeP,
-  print_registrationsP,
-  print_attributesP, print_rulesP, print_induct_rulesP,
-  print_trans_rulesP, print_methodsP, print_antiquotationsP,
-  thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
-  print_casesP, print_introsP, print_thmsP, print_prfsP, print_full_prfsP,
-  print_propP, print_termP, print_typeP,
+  redoP, undos_proofP, undoP, killP, interpretationP, interpretP,
+  instantiateP, (*diagnostic commands*) pretty_setmarginP,
+  print_commandsP, print_contextP, print_theoryP, print_syntaxP,
+  print_theoremsP, print_localesP, print_localeP,
+  print_registrationsP, print_attributesP, print_simpsetP,
+  print_rulesP, print_induct_rulesP, print_trans_rulesP,
+  print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP,
+  print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP,
+  print_full_prfsP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
@@ -845,7 +833,6 @@
   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
 
 (*these commands can be hidden in LaTeX output*)
-
 val hidden_commands = [
   "use", "ML", "ML_command", "ML_setup", "setup", "method_setup",
   "parse_ast_translation", "parse_translation", "print_translation",
@@ -853,8 +840,6 @@
 
 end;
 
-
-(*install the Pure outer syntax*)
 OuterSyntax.add_keywords IsarSyn.keywords;
 OuterSyntax.add_parsers IsarSyn.parsers;
 IsarOutput.add_hidden_commands IsarSyn.hidden_commands;