| changeset 21364 | 3baf57a27269 |
| parent 21319 | cf814e36f788 |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/FunDef.thy Tue Nov 14 17:55:30 2006 +0100 +++ b/src/HOL/FunDef.thy Tue Nov 14 22:16:54 2006 +0100 @@ -48,8 +48,8 @@ inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" -intros - accPI: "(!!y. r y x ==> accP r y) ==> accP r x" +where + accPI: "(!!y. r y x ==> accP r y) ==> accP r x" theorem accP_induct: