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/SN.thy
changeset 26932 c398a3866082
parent 26772 9174c7afd8b8
child 26966 071f40487734 
--- a/src/HOL/Nominal/Examples/SN.thy	Sat May 17 15:31:42 2008 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Sat May 17 21:46:22 2008 +0200
@@ -374,7 +374,7 @@
       then have a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2" by simp
       from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4) 
       moreover
-      have "NEUT (Var a)" by (force simp add: NEUT_def)
+      fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
       moreover
       have "NORMAL (Var a)" by (rule NORMAL_Var)
       ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
isabelle