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.
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
authorblanchet
Wed, 09 Feb 2022 10:47:34 +0100
changeset 75065 7cadf5a7ed5b
parent 75064 41fd2e8f6b16
child 75066 fe81645c0b40
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 07 16:59:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Feb 09 10:47:34 2022 +0100
@@ -343,7 +343,9 @@
 val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
 val parse_fact_override_chunk =
   (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
+  || (Args.add |-- Args.colon |-- Scan.succeed [] >> add_fact_override)
   || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
+  || (Args.del |-- Args.colon |-- Scan.succeed [] >> del_fact_override)
   || (parse_fact_refs >> only_fact_override)
 val parse_fact_override =
   Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides))
isabelle