1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Sep 11 12:31:05 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Sep 11 12:31:42 2010 +0200
1.3 @@ -29,7 +29,7 @@
1.4 val _ =
1.5 ProofGeneralPgip.add_preference Preferences.category_tracing
1.6 (Preferences.bool_pref auto "auto-sledgehammer"
1.7 - "Whether to run Sledgehammer automatically.")
1.8 + "Run Sledgehammer automatically.")
1.9
1.10 (** Sledgehammer commands **)
1.11
1.12 @@ -153,7 +153,6 @@
1.13 SOME s => parse_bool_option option name s
1.14 | NONE => default_value
1.15 val lookup_bool = the o general_lookup_bool false (SOME false)
1.16 - val lookup_bool_option = general_lookup_bool true NONE
1.17 fun lookup_time name =
1.18 case lookup name of
1.19 SOME s => parse_time_option name s