# HG changeset patch
# User nipkow
# Date 1047392367 -3600
# Node ID a077513c9a07828f4bf7e82c4b6c3e21975268e7
# Parent  11d7c5a8dbb79bc98ffa4e991f51e22bab40fdda
*** empty log message ***

diff -r 11d7c5a8dbb7 -r a077513c9a07 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 11 15:04:24 2003 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 11 15:19:27 2003 +0100
@@ -297,7 +297,8 @@
 
 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
   Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
-  Hoare/Pointers.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML
+  Hoare/Pointers.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
+  Hoare/ExamplesAbort.thy Hoare/hoareAbort.ML Hoare/HoareAbort.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Hoare
 
 
diff -r 11d7c5a8dbb7 -r a077513c9a07 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Mar 11 15:04:24 2003 +0100
+++ b/src/HOL/Set.thy	Tue Mar 11 15:19:27 2003 +0100
@@ -77,8 +77,10 @@
   "{x. P}"      == "Collect (%x. P)"
   "UN x y. B"   == "UN x. UN y. B"
   "UN x. B"     == "UNION UNIV (%x. B)"
+  "UN x. B"     == "UN x:UNIV. B"
   "INT x y. B"  == "INT x. INT y. B"
   "INT x. B"    == "INTER UNIV (%x. B)"
+  "INT x. B"    == "INT x:UNIV. B"
   "UN x:A. B"   == "UNION A (%x. B)"
   "INT x:A. B"  == "INTER A (%x. B)"
   "ALL x:A. P"  == "Ball A (%x. P)"
@@ -157,7 +159,8 @@
     let val (x,t) = atomic_abs_tr' abs
     in Syntax.const syn $ x $ A $ t end
 in
-[("Ball", btr' "_Ball"),("Bex", btr' "_Bex")]
+[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
+ ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
 end
 *}