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/Nominal/Examples/Compile.thy
changeset 22541 c33b542394f3
parent 22418 49e2d9744ae1
child 22829 f1db55c7534d 
--- a/src/HOL/Nominal/Examples/Compile.thy	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Wed Mar 28 18:25:23 2007 +0200
@@ -130,7 +130,7 @@
   and   x::"name"
   shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])"
   apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct)
-  apply (simp_all add: Isubst.simps eqvt fresh_bij)
+  apply (simp_all add: Isubst.simps eqvts fresh_bij)
   done
 
 lemma Isubst_supp:
isabelle