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.
Replaced application of subst by simplesubst in proof of app_Var_NF
authorberghofe
Wed, 02 Feb 2005 18:20:31 +0100
changeset 15490 2a183ef25fb1
parent 15489 d136af442665
child 15491 7c1f6e84f4ad
Replaced application of subst by simplesubst in proof of app_Var_NF to avoid problems with program extraction.
src/HOL/Lambda/WeakNorm.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lambda/WeakNorm.thy	Wed Feb 02 18:19:43 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Feb 02 18:20:31 2005 +0100
@@ -134,7 +134,7 @@
 
 lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
   apply (induct set: NF)
-  apply (subst app_last)
+  apply (simplesubst app_last)
   apply (rule exI)
   apply (rule conjI)
   apply (rule rtrancl_refl)
isabelle