1.1 --- a/src/HOL/IsaMakefile	Tue Mar 11 15:04:24 2003 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Mar 11 15:19:27 2003 +0100
     1.3 @@ -297,7 +297,8 @@
     1.4  
     1.5  $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
     1.6    Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
     1.7 -  Hoare/Pointers.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML
     1.8 +  Hoare/Pointers.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
     1.9 +  Hoare/ExamplesAbort.thy Hoare/hoareAbort.ML Hoare/HoareAbort.thy
    1.10  	@$(ISATOOL) usedir $(OUT)/HOL Hoare
    1.11  
    1.12  

     2.1 --- a/src/HOL/Set.thy	Tue Mar 11 15:04:24 2003 +0100
     2.2 +++ b/src/HOL/Set.thy	Tue Mar 11 15:19:27 2003 +0100
     2.3 @@ -77,8 +77,10 @@
     2.4    "{x. P}"      == "Collect (%x. P)"
     2.5    "UN x y. B"   == "UN x. UN y. B"
     2.6    "UN x. B"     == "UNION UNIV (%x. B)"
     2.7 +  "UN x. B"     == "UN x:UNIV. B"
     2.8    "INT x y. B"  == "INT x. INT y. B"
     2.9    "INT x. B"    == "INTER UNIV (%x. B)"
    2.10 +  "INT x. B"    == "INT x:UNIV. B"
    2.11    "UN x:A. B"   == "UNION A (%x. B)"
    2.12    "INT x:A. B"  == "INTER A (%x. B)"
    2.13    "ALL x:A. P"  == "Ball A (%x. P)"
    2.14 @@ -157,7 +159,8 @@
    2.15      let val (x,t) = atomic_abs_tr' abs
    2.16      in Syntax.const syn $ x $ A $ t end
    2.17  in
    2.18 -[("Ball", btr' "_Ball"),("Bex", btr' "_Bex")]
    2.19 +[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
    2.20 + ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
    2.21  end
    2.22  *}
    2.23