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/boogie.ML
changeset 61424 c3658c18b7bc
parent 59936 b8ffc3dc9e24
child 67399 eab6ce8368fa 
--- a/src/HOL/SMT_Examples/boogie.ML	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML	Tue Oct 13 09:21:15 2015 +0200
@@ -243,7 +243,7 @@
   end
 
 val boogie_rules =
-  [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
+  [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}] @
   [@{thm fun_upd_same}, @{thm fun_upd_apply}]
 
 fun boogie_tac ctxt axioms =
isabelle