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.
rename INF_drop_prefix to INFM_drop_prefix
authorhuffman
Thu, 04 Sep 2008 17:21:49 +0200
changeset 28132 236e07d8821e
parent 28131 3130d7b3149d
child 28133 218252dfd81e
rename INF_drop_prefix to INFM_drop_prefix
src/HOL/SizeChange/Correctness.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/SizeChange/Correctness.thy	Thu Sep 04 17:19:57 2008 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Thu Sep 04 17:21:49 2008 +0200
@@ -934,7 +934,7 @@
 
 
 
-lemma INF_drop_prefix:
+lemma INFM_drop_prefix:
   "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)"
   apply (auto simp:INFM_nat)
   apply (drule_tac x = "max m n" in spec)
@@ -1076,7 +1076,7 @@
   
   from ths_spec2(2)
   have "\<exists>\<^sub>\<infinity>i. n < i \<and> is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
-    unfolding INF_drop_prefix .
+    unfolding INFM_drop_prefix .
   
   hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))"
     apply (rule INFM_mono)
isabelle