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/Pattern.thy
changeset 45129 1fce03e3e8ad
parent 44687 20deab90494e
child 53015 a1119cf551e8 
--- a/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 12 20:16:48 2011 +0200
@@ -653,7 +653,7 @@
   shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and>
     set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
   using assms
-proof (induct p arbitrary: q t u \<Delta>)
+proof (induct p arbitrary: q t u)
   case (PVar x T)
   note PVar' = this
   show ?case
isabelle