--- 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
--- 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
*}