# HG changeset patch # User wenzelm # Date 1435323834 -7200 # Node ID 479071e8778f54dff4bda63842e80a43267bc1ff # Parent b5622eef7176df34c3e18d7fac0f72c476baad1d tuned proofs; diff -r b5622eef7176 -r 479071e8778f src/HOL/TLA/Stfun.thy --- 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