682 P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp || |
682 P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp || |
683 P.term >> FindTheorems.Pattern; |
683 P.term >> FindTheorems.Pattern; |
684 |
684 |
685 val find_theoremsP = |
685 val find_theoremsP = |
686 OuterSyntax.improper_command "find_theorems" |
686 OuterSyntax.improper_command "find_theorems" |
687 "print theorems meeting specified criteria" K.diag |
|
688 (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) -- |
|
689 Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) |
|
690 >> (Toplevel.no_timing oo IsarCmd.find_theorems)); |
|
691 |
|
692 val thms_containingP = (* FIXME legacy *) |
|
693 OuterSyntax.improper_command "thms_containing" |
|
694 "print theorems meeting specified criteria" K.diag |
687 "print theorems meeting specified criteria" K.diag |
695 (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) -- |
688 (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) -- |
696 Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) |
689 Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) |
697 >> (Toplevel.no_timing oo IsarCmd.find_theorems)); |
690 >> (Toplevel.no_timing oo IsarCmd.find_theorems)); |
698 |
691 |
866 print_commandsP, print_contextP, print_theoryP, print_syntaxP, |
859 print_commandsP, print_contextP, print_theoryP, print_syntaxP, |
867 print_theoremsP, print_localesP, print_localeP, |
860 print_theoremsP, print_localesP, print_localeP, |
868 print_registrationsP, print_attributesP, print_simpsetP, |
861 print_registrationsP, print_attributesP, print_simpsetP, |
869 print_rulesP, print_induct_rulesP, print_trans_rulesP, |
862 print_rulesP, print_induct_rulesP, print_trans_rulesP, |
870 print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP, |
863 print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP, |
871 thms_containingP, (* FIXME legacy *) |
|
872 print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP, |
864 print_bindsP, print_lthmsP, print_casesP, print_thmsP, print_prfsP, |
873 print_full_prfsP, print_propP, print_termP, print_typeP, |
865 print_full_prfsP, print_propP, print_termP, print_typeP, |
874 (*system commands*) |
866 (*system commands*) |
875 cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, |
867 cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, |
876 touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, |
868 touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, |