Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 55183 17ec4a29ef71
parent 54816 10d48c2a3e32 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jan 30 14:37:53 2014 +0100
@@ -94,8 +94,8 @@
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
    ("isar_proofs", "smart"),
-   ("isar_compress", "10"),
-   ("isar_try0", "true"),
+   ("compress_isar", "10"),
+   ("try0_isar", "true"),
    ("slice", "true"),
    ("minimize", "smart"),
    ("preplay_timeout", "3")]
@@ -103,7 +103,7 @@
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),
-   ("dont_compress_isar", ("isar_compress", ["0"])),
+   ("dont_compress_isar", ("compress_isar", ["0"])),
    ("isar_proof", ("isar_proofs", [])) (* legacy *)]
 val negated_alias_params =
   [("no_debug", "debug"),
@@ -117,7 +117,7 @@
    ("no_isar_proofs", "isar_proofs"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize"),
-   ("dont_try0_isar", "isar_try0")]
+   ("dont_try0_isar", "try0_isar")]
 
 val params_not_for_minimize =
   ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
@@ -286,8 +286,8 @@
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
-    val isar_compress = Real.max (1.0, lookup_real "isar_compress")
-    val isar_try0 = lookup_bool "isar_try0"
+    val compress_isar = Real.max (1.0, lookup_real "compress_isar")
+    val try0_isar = lookup_bool "try0_isar"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
     val timeout = lookup_time "timeout"
@@ -299,7 +299,7 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, minimize = minimize,
+     compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
isabelle