# HG changeset patch # User wenzelm # Date 1316524050 -7200 # Node ID 8a4db903039fdd16fba0ebd1e5107db0e244194b # Parent 99e1965f9c21e7a1cd41b5fdcfbea2ccc4dd32f3 proper fact binding; diff -r 99e1965f9c21 -r 8a4db903039f src/CCL/ex/List.thy --- a/src/CCL/ex/List.thy Tue Sep 20 09:30:19 2011 +0200 +++ b/src/CCL/ex/List.thy Tue Sep 20 15:07:30 2011 +0200 @@ -19,7 +19,7 @@ where "l @ m == lrec(l,m,%x xs g. x$g)" axiomatization member :: "[i,i]=>i" (infixr "mem" 55) (* FIXME dangling eq *) - where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" + where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" definition filter :: "[i,i]=>i" where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"