# 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: "(\\<^sub>\i::nat. i > n \ P i) = (\\<^sub>\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 "\\<^sub>\i. n < i \ is_desc_fthread (\s i) p (s i) (s (Suc i))" - unfolding INF_drop_prefix . + unfolding INFM_drop_prefix . hence p2: "\\<^sub>\i. is_desc_fthread ?j\ p (s i) (s (Suc i))" apply (rule INFM_mono)