comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
authorblanchet
Mon Sep 27 09:17:24 2010 +0200 (2010-09-27)
changeset 39719b876d7525e72
parent 39718 6e8c231876f5
child 39720 0b93a954da4f
comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
src/HOL/HOL.thy
src/HOL/Tools/try.ML
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 27 09:14:39 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 27 09:17:24 2010 +0200
     1.3 @@ -1980,9 +1980,11 @@
     1.4  *} "solve goal by normalization"
     1.5  
     1.6  
     1.7 +(*
     1.8  subsection {* Try *}
     1.9  
    1.10  setup {* Try.setup *}
    1.11 +*)
    1.12  
    1.13  subsection {* Counterexample Search Units *}
    1.14  
     2.1 --- a/src/HOL/Tools/try.ML	Mon Sep 27 09:14:39 2010 +0200
     2.2 +++ b/src/HOL/Tools/try.ML	Mon Sep 27 09:17:24 2010 +0200
     2.3 @@ -2,18 +2,25 @@
     2.4      Author:     Jasmin Blanchette, TU Muenchen
     2.5  
     2.6  Try a combination of proof methods.
     2.7 +
     2.8 +FIXME: reintroduce or remove commented code (see also HOL.thy)
     2.9  *)
    2.10  
    2.11  signature TRY =
    2.12  sig
    2.13 +(*
    2.14    val auto : bool Unsynchronized.ref
    2.15 +*)
    2.16    val invoke_try : Time.time option -> Proof.state -> bool
    2.17 +(*
    2.18    val setup : theory -> theory
    2.19 +*)
    2.20  end;
    2.21  
    2.22  structure Try : TRY =
    2.23  struct
    2.24  
    2.25 +(*
    2.26  val auto = Unsynchronized.ref false
    2.27  
    2.28  val _ =
    2.29 @@ -21,6 +28,7 @@
    2.30    (Unsynchronized.setmp auto true (fn () =>
    2.31      Preferences.bool_pref auto
    2.32        "auto-try" "Try standard proof methods.") ());
    2.33 +*)
    2.34  
    2.35  val default_timeout = Time.fromSeconds 5
    2.36  
    2.37 @@ -108,8 +116,10 @@
    2.38        (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
    2.39                                      o Toplevel.proof_of)))
    2.40  
    2.41 +(*
    2.42  fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
    2.43  
    2.44  val setup = Auto_Tools.register_tool (tryN, auto_try)
    2.45 +*)
    2.46  
    2.47  end;