fixed set comprehension print translation
authornipkow
Sun Jan 28 16:46:19 2001 +0100 (2001-01-28)
changeset 1098565a8a0e2d55b
parent 10984 8f49dcbec859
child 10986 616bcfc7b848
fixed set comprehension print translation
src/HOL/IsaMakefile
src/HOL/Set.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 26 15:50:52 2001 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sun Jan 28 16:46:19 2001 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4    Library/Quotient.thy Library/Ring_and_Field.thy \
     1.5    Library/Ring_and_Field_Example.thy Library/README.html \
     1.6    Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
     1.7 -  Library/While_Combinator.thy Library/While_Combinator_Example.thy
     1.8 +  Library/While_Combinator.thy
     1.9  	@$(ISATOOL) usedir $(OUT)/HOL Library
    1.10  
    1.11  
     2.1 --- a/src/HOL/Set.thy	Fri Jan 26 15:50:52 2001 +0100
     2.2 +++ b/src/HOL/Set.thy	Sun Jan 28 16:46:19 2001 +0100
     2.3 @@ -184,9 +184,9 @@
     2.4  
     2.5  fun setcompr_tr'[Abs(_,_,P)] =
     2.6    let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
     2.7 -        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
     2.8 -            if n>0 andalso m=n andalso
     2.9 -              ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
    2.10 +        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ P, n) =
    2.11 +            if n>0 andalso m=n andalso not(loose_bvar1(P,n)) andalso
    2.12 +               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
    2.13              then () else raise Match
    2.14  
    2.15        fun tr'(_ $ abs) =