changeset 23746 | a455e69c31cc |
parent 21020 | 9af9ceb16d58 |
child 27362 | a6dc1769fdda |
--- a/src/HOL/IMP/Denotation.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Denotation.thy Wed Jul 11 11:14:51 2007 +0200 @@ -62,7 +62,7 @@ apply fast (* while *) -apply (erule lfp_induct_set [OF _ Gamma_mono]) +apply (erule lfp_induct2 [OF _ Gamma_mono]) apply (unfold Gamma_def) apply fast done