1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Sep 28 18:55:37 2001 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Sep 28 19:17:01 2001 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  *}
     1.5  
     1.6  consts while_aux :: "('a => bool) \<times> ('a => 'a) \<times> 'a => 'a"
     1.7 -recdef while_aux
     1.8 +recdef (permissive) while_aux
     1.9    "same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c.
    1.10        {(t, s).  b s \<and> c s = t \<and>
    1.11          \<not> (\<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"