| changeset 21020 | 9af9ceb16d58 |
| parent 20503 | 503ac4c5ef91 |
| child 23746 | a455e69c31cc |
--- a/src/HOL/IMP/Denotation.thy Fri Oct 13 18:14:12 2006 +0200 +++ b/src/HOL/IMP/Denotation.thy Fri Oct 13 18:15:18 2006 +0200 @@ -62,7 +62,7 @@ apply fast (* while *) -apply (erule lfp_induct [OF _ Gamma_mono]) +apply (erule lfp_induct_set [OF _ Gamma_mono]) apply (unfold Gamma_def) apply fast done