| changeset 26304 | 02fbd0e7954a |
| parent 19763 | ec18656a2c10 |
| child 27101 | 864d29f11c9d |
--- a/src/HOLCF/FOCUS/Buffer_adm.thy Mon Mar 17 18:37:04 2008 +0100 +++ b/src/HOLCF/FOCUS/Buffer_adm.thy Mon Mar 17 18:37:05 2008 +0100 @@ -233,7 +233,7 @@ (**** new approach for admissibility, reduces itself to absurdity *************) -lemma adm_BufAC_Asm: "adm (\<lambda>x. x\<in>BufAC_Asm)" +lemma adm_BufAC_Asm': "adm (\<lambda>x. x\<in>BufAC_Asm)" apply (rule def_gfp_admI) apply (rule BufAC_Asm_def [THEN eq_reflection]) apply (safe)