# HG changeset patch
# User wenzelm
# Date 1125583091 -7200
# Node ID 515badbfc4d6332e8430877fa5a1bf0a3c34447f
# Parent  64242b791c19a625545b2b9c6cf0bcddea36d796
renamed 'thms_containing' to 'find_theorems' -- keep old version for the time being;

diff -r 64242b791c19 -r 515badbfc4d6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Sep 01 15:58:10 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Sep 01 15:58:11 2005 +0200
@@ -692,6 +692,13 @@
   P.term >> FindTheorems.Pattern;
 
 val find_theoremsP =
+  OuterSyntax.improper_command "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 thms_containingP =   (* FIXME legacy *)
   OuterSyntax.improper_command "thms_containing"
     "print theorems meeting specified criteria" K.diag
     (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
@@ -870,6 +877,7 @@
   print_registrationsP, print_attributesP, print_simpsetP,
   print_rulesP, print_induct_rulesP, print_trans_rulesP,
   print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP,
+  thms_containingP,  (* FIXME legacy *)
   print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP,
   print_full_prfsP, print_propP, print_termP, print_typeP,
   (*system commands*)