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
```