src/HOL/SMT_Examples/SMT_Tests.thy
changeset 61424 c3658c18b7bc
parent 58889 5b7a9633cfa8
child 61945 1135b8de26c3
     1.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -506,7 +506,7 @@
     1.4    "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
     1.5    "(fst (x, y) = snd (x, y)) = (x = y)"
     1.6    "(fst p = snd p) = (p = (snd p, fst p))"
     1.7 -  using fst_conv snd_conv pair_collapse
     1.8 +  using fst_conv snd_conv prod.collapse
     1.9    by smt+
    1.10  
    1.11  lemma
    1.12 @@ -525,7 +525,7 @@
    1.13  lemma
    1.14    "fst (hd [(a, b)]) = a"
    1.15    "snd (hd [(a, b)]) = b"
    1.16 -  using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps
    1.17 +  using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
    1.18    by smt+
    1.19  
    1.20  
    1.21 @@ -627,7 +627,7 @@
    1.22    "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
    1.23    "(fst (x, y) = snd (x, y)) = (x = y)"
    1.24    "(fst p = snd p) = (p = (snd p, fst p))"
    1.25 -  using fst_conv snd_conv pair_collapse
    1.26 +  using fst_conv snd_conv prod.collapse
    1.27    using [[smt_oracle, z3_extensions]]
    1.28    by smt+
    1.29  
    1.30 @@ -648,7 +648,7 @@
    1.31  lemma
    1.32    "fst (hd [(a, b)]) = a"
    1.33    "snd (hd [(a, b)]) = b"
    1.34 -  using fst_conv snd_conv pair_collapse list.sel(1,3)
    1.35 +  using fst_conv snd_conv prod.collapse list.sel(1,3)
    1.36    using [[smt_oracle, z3_extensions]]
    1.37    by smt+
    1.38