src/HOL/Tools/refute.ML
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18760 97aaecb84afe
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  	val refute_term    : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model that refutes a formula *)
     1.5  	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
     1.6  
     1.7 -	val setup : (theory -> theory) list
     1.8 +	val setup : theory -> theory
     1.9  end;
    1.10  
    1.11  structure Refute : REFUTE =
    1.12 @@ -2605,25 +2605,25 @@
    1.13  	(* (theory -> theory) list *)
    1.14  
    1.15  	val setup =
    1.16 -		[RefuteData.init,
    1.17 -		 add_interpreter "stlc"    stlc_interpreter,
    1.18 -		 add_interpreter "Pure"    Pure_interpreter,
    1.19 -		 add_interpreter "HOLogic" HOLogic_interpreter,
    1.20 -		 add_interpreter "set"     set_interpreter,
    1.21 -		 add_interpreter "IDT"             IDT_interpreter,
    1.22 -		 add_interpreter "IDT_constructor" IDT_constructor_interpreter,
    1.23 -		 add_interpreter "IDT_recursion"   IDT_recursion_interpreter,
    1.24 -		 add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter,
    1.25 -		 add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter,
    1.26 -		 add_interpreter "Nat.op <" Nat_less_interpreter,
    1.27 -		 add_interpreter "Nat.op +" Nat_plus_interpreter,
    1.28 -		 add_interpreter "Nat.op -" Nat_minus_interpreter,
    1.29 -		 add_interpreter "Nat.op *" Nat_mult_interpreter,
    1.30 -		 add_interpreter "List.op @" List_append_interpreter,
    1.31 -		 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter,
    1.32 -		 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter,
    1.33 -		 add_printer "stlc" stlc_printer,
    1.34 -		 add_printer "set"  set_printer,
    1.35 -		 add_printer "IDT"  IDT_printer];
    1.36 +		 RefuteData.init #>
    1.37 +		 add_interpreter "stlc"    stlc_interpreter #>
    1.38 +		 add_interpreter "Pure"    Pure_interpreter #>
    1.39 +		 add_interpreter "HOLogic" HOLogic_interpreter #>
    1.40 +		 add_interpreter "set"     set_interpreter #>
    1.41 +		 add_interpreter "IDT"             IDT_interpreter #>
    1.42 +		 add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
    1.43 +		 add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
    1.44 +		 add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
    1.45 +		 add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter #>
    1.46 +		 add_interpreter "Nat.op <" Nat_less_interpreter #>
    1.47 +		 add_interpreter "Nat.op +" Nat_plus_interpreter #>
    1.48 +		 add_interpreter "Nat.op -" Nat_minus_interpreter #>
    1.49 +		 add_interpreter "Nat.op *" Nat_mult_interpreter #>
    1.50 +		 add_interpreter "List.op @" List_append_interpreter #>
    1.51 +		 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
    1.52 +		 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
    1.53 +		 add_printer "stlc" stlc_printer #>
    1.54 +		 add_printer "set"  set_printer #>
    1.55 +		 add_printer "IDT"  IDT_printer;
    1.56  
    1.57  end