equal
deleted
inserted
replaced
808 |
808 |
809 val find_theoremsP = |
809 val find_theoremsP = |
810 OuterSyntax.improper_command "find_theorems" |
810 OuterSyntax.improper_command "find_theorems" |
811 "print theorems meeting specified criteria" K.diag |
811 "print theorems meeting specified criteria" K.diag |
812 (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) -- |
812 (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) -- |
|
813 Scan.optional (P.reserved "with_dups" >> K false) true -- |
813 Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) |
814 Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) |
814 >> (Toplevel.no_timing oo IsarCmd.find_theorems)); |
815 >> (Toplevel.no_timing oo IsarCmd.find_theorems)); |
815 |
816 |
816 val print_bindsP = |
817 val print_bindsP = |
817 OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag |
818 OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag |