proper fact binding;
authorwenzelm
Tue, 20 Sep 2011 15:07:30 +0200
changeset 45010 8a4db903039f
parent 45009 99e1965f9c21
child 45011 436ea69d5d37
proper fact binding;
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)"