src/HOL/Tools/SMT/z3_proof_tools.ML
changeset 40681 872b08416fb4
parent 40663 e080c9e68752
child 40806 59d96f777da3
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Nov 24 08:51:48 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Nov 24 10:39:58 2010 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4        | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
     1.5        | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
     1.6        | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
     1.7 -      | Const (@{const_name SMT.distinct}, _) $ _ =>
     1.8 +      | Const (@{const_name distinct}, _) $ _ =>
     1.9            if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
    1.10            else fresh_abstraction cvs ct
    1.11        | Const (@{const_name If}, _) $ _ $ _ $ _ =>
    1.12 @@ -258,9 +258,9 @@
    1.13      (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
    1.14      (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
    1.15  
    1.16 -  val dist1 = @{lemma "SMT.distinct [] == ~False" by (simp add: distinct_def)}
    1.17 -  val dist2 = @{lemma "SMT.distinct [x] == ~False" by (simp add: distinct_def)}
    1.18 -  val dist3 = @{lemma "SMT.distinct (x # xs) == x ~: set xs & distinct xs"
    1.19 +  val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)}
    1.20 +  val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)}
    1.21 +  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
    1.22      by (simp add: distinct_def)}
    1.23  
    1.24    fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2