Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
find_theorems: moved with_dup into the brackets, i.e.
authorkleing
Tue, 06 Mar 2007 05:31:23 +0100
changeset 22415 c310ca7cd47f
parent 22414 3f189ea9bfe7
child 22416 4af50522be35
find_theorems: moved with_dup into the brackets, i.e. find_theorems (20 with_dups) "some term" ..
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 06 05:09:53 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 06 05:31:23 2007 +0100
@@ -809,8 +809,10 @@
 val find_theoremsP =
   OuterSyntax.improper_command "find_theorems"
     "print theorems meeting specified criteria" K.diag
-    (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
-     Scan.optional (P.reserved "with_dups" >> K false) true -- 
+    (Scan.optional (P.$$$ "(" |-- P.!!!
+                        (Scan.option P.nat --
+                         Scan.optional (P.reserved "with_dups" >> K false) true
+                         --| P.$$$ ")")) (NONE, false) --
      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
isabelle