--- a/src/ZF/Induct/Brouwer.thy Thu Jun 21 17:28:53 2007 +0200
+++ b/src/ZF/Induct/Brouwer.thy Thu Jun 21 20:07:26 2007 +0200
@@ -32,10 +32,12 @@
-- {* A nicer induction rule than the standard one. *}
using b
apply induct
- apply (assumption | rule cases)+
- apply (fast elim: fun_weaken_type)
- apply (fast dest: apply_type)
- done
+ apply (rule cases(1))
+ apply (erule (1) cases(2))
+ apply (rule cases(3))
+ apply (fast elim: fun_weaken_type)
+ apply (fast dest: apply_type)
+ done
subsection {* The Martin-Löf wellordering type *}