# HG changeset patch
# User wenzelm
# Date 938357185 -7200
# Node ID f677cdc7fae9cbc8153e07b4fd7ada4ab33a8a9d
# Parent  c650147f56f1541d383ba6af7396ad55f700b171
added 'thms_containing', 'ML_setup';

diff -r c650147f56f1 -r f677cdc7fae9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Sep 26 16:45:00 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Sep 26 16:46:25 1999 +0200
@@ -200,11 +200,15 @@
     (P.name >> IsarCmd.use);
 
 val mlP =
-  OuterSyntax.command "ML" "eval ML text" K.diag
-    (P.text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
+  OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
+    (P.text >> IsarCmd.use_mltext)
+
+val ml_setupP =
+  OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
+    (P.text >> IsarCmd.use_mltext_theory);
 
 val setupP =
-  OuterSyntax.command "setup" "apply ML theory transformer" K.thy_decl
+  OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
     (P.text >> (Toplevel.theory o IsarThy.use_setup));
 
 
@@ -465,6 +469,10 @@
   OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
     (Scan.succeed IsarCmd.print_methods);
 
+val thms_containingP =
+  OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants"
+    K.diag (Scan.repeat P.xname >> IsarCmd.print_thms_containing);
+
 val print_bindsP =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed IsarCmd.print_binds);
@@ -585,10 +593,10 @@
   (*theory sections*)
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
-  constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP, setupP,
-  parse_ast_translationP, parse_translationP, print_translationP,
-  typed_print_translationP, print_ast_translationP,
-  token_translationP, oracleP,
+  constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP,
+  ml_setupP, setupP, parse_ast_translationP, parse_translationP,
+  print_translationP, typed_print_translationP,
+  print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
@@ -597,9 +605,9 @@
   cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
-  print_syntaxP, print_attributesP, print_methodsP, print_theoremsP,
-  print_bindsP, print_lthmsP, print_thmsP, print_propP, print_termP,
-  print_typeP,
+  print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
+  thms_containingP, print_bindsP, print_lthmsP, print_thmsP,
+  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, remove_thyP, prP, disable_prP,