# HG changeset patch
# User huffman
# Date 1220541709 -7200
# Node ID 236e07d8821ef8dcc26096732b7744f21aeedb9e
# Parent  3130d7b3149d5ccb2fb490671dc6a3e27a7f4604
rename INF_drop_prefix to INFM_drop_prefix

diff -r 3130d7b3149d -r 236e07d8821e src/HOL/SizeChange/Correctness.thy
--- 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)