src/HOL/Refute.thy
changeset 46960 f19e5837ad69
parent 46950 d0181abdbdac
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Refute.thy	Fri Mar 16 14:42:11 2012 +0100
     1.2 +++ b/src/HOL/Refute.thy	Fri Mar 16 14:46:13 2012 +0100
     1.3 @@ -15,6 +15,15 @@
     1.4  
     1.5  setup Refute.setup
     1.6  
     1.7 +refute_params
     1.8 + [itself = 1,
     1.9 +  minsize = 1,
    1.10 +  maxsize = 8,
    1.11 +  maxvars = 10000,
    1.12 +  maxtime = 60,
    1.13 +  satsolver = auto,
    1.14 +  no_assms = false]
    1.15 +
    1.16  text {*
    1.17  \small
    1.18  \begin{verbatim}
    1.19 @@ -80,8 +89,6 @@
    1.20  (* "expect"      string  Expected result ("genuine", "potential", "none", or *)
    1.21  (*                       "unknown").                                         *)
    1.22  (*                                                                           *)
    1.23 -(* See 'HOL/SAT.thy' for default values.                                     *)
    1.24 -(*                                                                           *)
    1.25  (* The size of particular types can be specified in the form type=size       *)
    1.26  (* (where 'type' is a string, and 'size' is an int).  Examples:              *)
    1.27  (* "'a"=1                                                                    *)