1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 27 14:56:26 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 27 14:56:28 2011 +0200
     1.3 @@ -85,6 +85,7 @@
     1.4     ("overlord", "false"),
     1.5     ("blocking", "false"),
     1.6     ("type_sys", "smart"),
     1.7 +   ("sound", "false"),
     1.8     ("relevance_thresholds", "0.45 0.85"),
     1.9     ("max_relevant", "smart"),
    1.10     ("max_mono_iters", "3"),
    1.11 @@ -101,11 +102,12 @@
    1.12     ("quiet", "verbose"),
    1.13     ("no_overlord", "overlord"),
    1.14     ("non_blocking", "blocking"),
    1.15 +   ("unsound", "sound"),
    1.16     ("no_isar_proof", "isar_proof"),
    1.17     ("no_slicing", "slicing")]
    1.18  
    1.19  val params_for_minimize =
    1.20 -  ["debug", "verbose", "overlord", "type_sys", "max_mono_iters",
    1.21 +  ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
    1.22     "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    1.23     "preplay_timeout"]
    1.24  
    1.25 @@ -122,7 +124,8 @@
    1.26      ss as _ :: _ => forall (is_prover_supported ctxt) ss
    1.27    | _ => false
    1.28  
    1.29 -(* Secret feature: "provers =" and "type_sys =" can be left out. *)
    1.30 +(* "provers =" and "type_sys =" can be left out. The latter is a secret
    1.31 +   feature. *)
    1.32  fun check_and_repair_raw_param ctxt (name, value) =
    1.33    if is_known_raw_param name then
    1.34      (name, value)
    1.35 @@ -267,6 +270,7 @@
    1.36        else case lookup_string "type_sys" of
    1.37          "smart" => NONE
    1.38        | s => SOME (type_sys_from_string s)
    1.39 +    val sound = mode = Auto_Try orelse lookup_bool "sound"
    1.40      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.41      val max_relevant = lookup_option lookup_int "max_relevant"
    1.42      val max_mono_iters = lookup_int "max_mono_iters"
    1.43 @@ -285,9 +289,9 @@
    1.44       provers = provers, relevance_thresholds = relevance_thresholds,
    1.45       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    1.46       max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
    1.47 -     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    1.48 -     slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
    1.49 -     expect = expect}
    1.50 +     sound = sound, isar_proof = isar_proof,
    1.51 +     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    1.52 +     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.53    end
    1.54  
    1.55  fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)