proper fact binding;
authorwenzelm
Tue Sep 20 15:07:30 2011 +0200 (2011-09-20)
changeset 450108a4db903039f
parent 45009 99e1965f9c21
child 45011 436ea69d5d37
proper fact binding;
src/CCL/ex/List.thy
     1.1 --- a/src/CCL/ex/List.thy	Tue Sep 20 09:30:19 2011 +0200
     1.2 +++ b/src/CCL/ex/List.thy	Tue Sep 20 15:07:30 2011 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    where "l @ m == lrec(l,m,%x xs g. x$g)"
     1.5  
     1.6  axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
     1.7 -  where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
     1.8 +  where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
     1.9  
    1.10  definition filter :: "[i,i]=>i"
    1.11    where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"