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.
merged
authorwenzelm
Fri, 27 Jul 2012 22:28:30 +0200
changeset 48569 56f652ac2d13
parent 48568 084cd758a8ab (current diff)
parent 48567 3c4d7ff75f01 (diff)
child 48570 0c32d6267b93
merged
--- a/src/HOL/Nominal/Examples/Class1.thy	Fri Jul 27 22:26:38 2012 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy	Fri Jul 27 22:28:30 2012 +0200
@@ -6791,7 +6791,7 @@
     apply(force)
     apply(rule exists_fresh'(1)[OF fs_name1])
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P},
-                                        M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)")
+                                        M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,y,x)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+
     apply(simp only: fresh_fun_simp_ImpL)
isabelle