src/HOL/Tools/refute.ML
changeset 34974 18b41bba42b5
parent 34120 f9920a3ddf50
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -708,13 +708,13 @@
     1.4        (* other optimizations *)
     1.5        | Const (@{const_name Finite_Set.card}, _) => t
     1.6        | Const (@{const_name Finite_Set.finite}, _) => t
     1.7 -      | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
     1.8 +      | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
     1.9          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
    1.10 -      | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
    1.11 +      | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
    1.12          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    1.13 -      | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
    1.14 +      | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
    1.15          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    1.16 -      | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
    1.17 +      | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
    1.18          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    1.19        | Const (@{const_name List.append}, _) => t
    1.20        | Const (@{const_name lfp}, _) => t
    1.21 @@ -883,16 +883,16 @@
    1.22        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
    1.23        | Const (@{const_name Finite_Set.finite}, T) =>
    1.24          collect_type_axioms T axs
    1.25 -      | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
    1.26 +      | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
    1.27          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    1.28            collect_type_axioms T axs
    1.29 -      | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
    1.30 +      | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
    1.31          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.32            collect_type_axioms T axs
    1.33 -      | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
    1.34 +      | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []),
    1.35          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.36            collect_type_axioms T axs
    1.37 -      | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
    1.38 +      | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []),
    1.39          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.40            collect_type_axioms T axs
    1.41        | Const (@{const_name List.append}, T) => collect_type_axioms T axs
    1.42 @@ -2765,13 +2765,13 @@
    1.43    (* theory -> model -> arguments -> Term.term ->
    1.44      (interpretation * model * arguments) option *)
    1.45  
    1.46 -  (* only an optimization: 'HOL.less' could in principle be interpreted with *)
    1.47 +  (* only an optimization: 'less' could in principle be interpreted with *)
    1.48    (* interpreters available already (using its definition), but the code     *)
    1.49    (* below is more efficient                                                 *)
    1.50  
    1.51    fun Nat_less_interpreter thy model args t =
    1.52      case t of
    1.53 -      Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
    1.54 +      Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
    1.55          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    1.56        let
    1.57          val size_of_nat = size_of_type thy model (Type ("nat", []))
    1.58 @@ -2788,13 +2788,13 @@
    1.59    (* theory -> model -> arguments -> Term.term ->
    1.60      (interpretation * model * arguments) option *)
    1.61  
    1.62 -  (* only an optimization: 'HOL.plus' could in principle be interpreted with *)
    1.63 +  (* only an optimization: 'plus' could in principle be interpreted with *)
    1.64    (* interpreters available already (using its definition), but the code     *)
    1.65    (* below is more efficient                                                 *)
    1.66  
    1.67    fun Nat_plus_interpreter thy model args t =
    1.68      case t of
    1.69 -      Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
    1.70 +      Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
    1.71          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.72        let
    1.73          val size_of_nat = size_of_type thy model (Type ("nat", []))
    1.74 @@ -2819,13 +2819,13 @@
    1.75    (* theory -> model -> arguments -> Term.term ->
    1.76      (interpretation * model * arguments) option *)
    1.77  
    1.78 -  (* only an optimization: 'HOL.minus' could in principle be interpreted *)
    1.79 +  (* only an optimization: 'minus' could in principle be interpreted *)
    1.80    (* with interpreters available already (using its definition), but the *)
    1.81    (* code below is more efficient                                        *)
    1.82  
    1.83    fun Nat_minus_interpreter thy model args t =
    1.84      case t of
    1.85 -      Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
    1.86 +      Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
    1.87          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.88        let
    1.89          val size_of_nat = size_of_type thy model (Type ("nat", []))
    1.90 @@ -2847,13 +2847,13 @@
    1.91    (* theory -> model -> arguments -> Term.term ->
    1.92      (interpretation * model * arguments) option *)
    1.93  
    1.94 -  (* only an optimization: 'HOL.times' could in principle be interpreted *)
    1.95 +  (* only an optimization: 'times' could in principle be interpreted *)
    1.96    (* with interpreters available already (using its definition), but the *)
    1.97    (* code below is more efficient                                        *)
    1.98  
    1.99    fun Nat_times_interpreter thy model args t =
   1.100      case t of
   1.101 -      Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
   1.102 +      Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
   1.103          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   1.104        let
   1.105          val size_of_nat = size_of_type thy model (Type ("nat", []))