Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT_Examples/SMT_Tests.thy
changeset 61424 c3658c18b7bc
parent 58889 5b7a9633cfa8
child 61945 1135b8de26c3 
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -506,7 +506,7 @@
   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
-  using fst_conv snd_conv pair_collapse
+  using fst_conv snd_conv prod.collapse
   by smt+
 
 lemma
@@ -525,7 +525,7 @@
 lemma
   "fst (hd [(a, b)]) = a"
   "snd (hd [(a, b)]) = b"
-  using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps
+  using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
   by smt+
 
 
@@ -627,7 +627,7 @@
   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
-  using fst_conv snd_conv pair_collapse
+  using fst_conv snd_conv prod.collapse
   using [[smt_oracle, z3_extensions]]
   by smt+
 
@@ -648,7 +648,7 @@
 lemma
   "fst (hd [(a, b)]) = a"
   "snd (hd [(a, b)]) = b"
-  using fst_conv snd_conv pair_collapse list.sel(1,3)
+  using fst_conv snd_conv prod.collapse list.sel(1,3)
   using [[smt_oracle, z3_extensions]]
   by smt+
isabelle