Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proofs;
authorwenzelm
Fri, 26 Jun 2015 15:03:54 +0200
changeset 60590 479071e8778f
parent 60589 b5622eef7176
child 60591 e0b77517f9a9
tuned proofs;
src/HOL/TLA/Stfun.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/TLA/Stfun.thy	Fri Jun 26 14:53:28 2015 +0200
+++ b/src/HOL/TLA/Stfun.thy	Fri Jun 26 15:03:54 2015 +0200
@@ -61,7 +61,7 @@
   apply (rule equalityI)
    apply (rule subset_UNIV)
   apply (rule subsetI)
-  apply (drule_tac c = "(xa, arbitrary) " in basevars)
+  apply (drule_tac c = "(xa, _) " in basevars)
   apply auto
   done
 
@@ -70,7 +70,7 @@
   apply (rule equalityI)
    apply (rule subset_UNIV)
   apply (rule subsetI)
-  apply (drule_tac c = "(arbitrary, xa) " in basevars)
+  apply (drule_tac c = "(_, xa) " in basevars)
   apply auto
   done
isabelle