# HG changeset patch
# User paulson
# Date 911398246 -3600
# Node ID 325300576da7a9ffcda566e0b766464b70b709ae
# Parent  41aa67a045f79fdf0beab07788fe7b0414b8bf30
Finally removing "Compl" from HOL

diff -r 41aa67a045f7 -r 325300576da7 NEWS
--- a/NEWS	Wed Nov 18 11:12:29 1998 +0100
+++ b/NEWS	Wed Nov 18 15:10:46 1998 +0100
@@ -5,6 +5,10 @@
 New in this Isabelle version
 ----------------------------
 
+*** Overview of INCOMPATIBILITIES (see below for more details) ***
+
+* HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
+
 *** General ***
 
 * tuned current_goals_markers semantics: begin / end goal avoids
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/Induct/Mutil.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -23,7 +23,7 @@
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
+    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
 
 defs
   below_def  "below n    == {i. i<n}"
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/Set.ML	Wed Nov 18 15:10:46 1998 +0100
@@ -299,7 +299,7 @@
 val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
 
 
-section "Set complement -- Compl";
+section "Set complement";
 
 qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
  (fn _ => [ (Blast_tac 1) ]);
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/Set.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -40,10 +40,6 @@
   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
 
 
-(*For compatibility: DELETE after one release*)
-syntax Compl :: ('a set) => 'a set   (*complement*)
-translations "Compl A"  => "- A"
-
 (** Additional concrete syntax **)
 
 syntax
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/UNITY/Lift.thy
--- a/src/HOL/UNITY/Lift.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/UNITY/Lift.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -36,10 +36,10 @@
     "queueing == above Un below"
 
   goingup :: state set
-    "goingup   == above Int  ({s. up s}  Un Compl below)"
+    "goingup   == above Int  ({s. up s}  Un -below)"
 
   goingdown :: state set
-    "goingdown == below Int ({s. ~ up s} Un Compl above)"
+    "goingdown == below Int ({s. ~ up s} Un -above)"
 
   ready :: state set
     "ready == {s. stop s & ~ open s & move s}"
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/UNITY/Token.thy
--- a/src/HOL/UNITY/Token.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/UNITY/Token.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -49,7 +49,7 @@
 
     TR4  "F : constrains (H i - HasTok i) (H i)"
 
-    TR5  "F : constrains (HasTok i) (HasTok i Un Compl(E i))"
+    TR5  "F : constrains (HasTok i) (HasTok i Un -(E i))"
 
     TR6  "F : leadsTo (H i Int HasTok i) (E i)"
 
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/UNITY/WFair.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -15,7 +15,7 @@
   (*This definition specifies weak fairness.  The rest of the theory
     is generic to all forms of fairness.*)
   transient :: "'a set => 'a program set"
-    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"
+    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
 
   ensures :: "['a set, 'a set] => 'a program set"
     "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/equalities.ML	Wed Nov 18 15:10:46 1998 +0100
@@ -336,7 +336,7 @@
 qed "Un_Diff_Int";
 
 
-section "Compl";
+section "Set complement";
 
 Goal "A Int -A = {}";
 by (Blast_tac 1);