Finally removing "Compl" from HOL
authorpaulson
Wed Nov 18 15:10:46 1998 +0100 (1998-11-18)
changeset 5931325300576da7
parent 5930 41aa67a045f7
child 5932 737559a43e71
Finally removing "Compl" from HOL
NEWS
src/HOL/Induct/Mutil.thy
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/UNITY/Lift.thy
src/HOL/UNITY/Token.thy
src/HOL/UNITY/WFair.thy
src/HOL/equalities.ML
     1.1 --- a/NEWS	Wed Nov 18 11:12:29 1998 +0100
     1.2 +++ b/NEWS	Wed Nov 18 15:10:46 1998 +0100
     1.3 @@ -5,6 +5,10 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Overview of INCOMPATIBILITIES (see below for more details) ***
     1.8 +
     1.9 +* HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
    1.10 +
    1.11  *** General ***
    1.12  
    1.13  * tuned current_goals_markers semantics: begin / end goal avoids
     2.1 --- a/src/HOL/Induct/Mutil.thy	Wed Nov 18 11:12:29 1998 +0100
     2.2 +++ b/src/HOL/Induct/Mutil.thy	Wed Nov 18 15:10:46 1998 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4  inductive "tiling A"
     2.5    intrs
     2.6      empty  "{} : tiling A"
     2.7 -    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
     2.8 +    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
     2.9  
    2.10  defs
    2.11    below_def  "below n    == {i. i<n}"
     3.1 --- a/src/HOL/Set.ML	Wed Nov 18 11:12:29 1998 +0100
     3.2 +++ b/src/HOL/Set.ML	Wed Nov 18 15:10:46 1998 +0100
     3.3 @@ -299,7 +299,7 @@
     3.4  val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
     3.5  
     3.6  
     3.7 -section "Set complement -- Compl";
     3.8 +section "Set complement";
     3.9  
    3.10  qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
    3.11   (fn _ => [ (Blast_tac 1) ]);
     4.1 --- a/src/HOL/Set.thy	Wed Nov 18 11:12:29 1998 +0100
     4.2 +++ b/src/HOL/Set.thy	Wed Nov 18 15:10:46 1998 +0100
     4.3 @@ -40,10 +40,6 @@
     4.4    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
     4.5  
     4.6  
     4.7 -(*For compatibility: DELETE after one release*)
     4.8 -syntax Compl :: ('a set) => 'a set   (*complement*)
     4.9 -translations "Compl A"  => "- A"
    4.10 -
    4.11  (** Additional concrete syntax **)
    4.12  
    4.13  syntax
     5.1 --- a/src/HOL/UNITY/Lift.thy	Wed Nov 18 11:12:29 1998 +0100
     5.2 +++ b/src/HOL/UNITY/Lift.thy	Wed Nov 18 15:10:46 1998 +0100
     5.3 @@ -36,10 +36,10 @@
     5.4      "queueing == above Un below"
     5.5  
     5.6    goingup :: state set
     5.7 -    "goingup   == above Int  ({s. up s}  Un Compl below)"
     5.8 +    "goingup   == above Int  ({s. up s}  Un -below)"
     5.9  
    5.10    goingdown :: state set
    5.11 -    "goingdown == below Int ({s. ~ up s} Un Compl above)"
    5.12 +    "goingdown == below Int ({s. ~ up s} Un -above)"
    5.13  
    5.14    ready :: state set
    5.15      "ready == {s. stop s & ~ open s & move s}"
     6.1 --- a/src/HOL/UNITY/Token.thy	Wed Nov 18 11:12:29 1998 +0100
     6.2 +++ b/src/HOL/UNITY/Token.thy	Wed Nov 18 15:10:46 1998 +0100
     6.3 @@ -49,7 +49,7 @@
     6.4  
     6.5      TR4  "F : constrains (H i - HasTok i) (H i)"
     6.6  
     6.7 -    TR5  "F : constrains (HasTok i) (HasTok i Un Compl(E i))"
     6.8 +    TR5  "F : constrains (HasTok i) (HasTok i Un -(E i))"
     6.9  
    6.10      TR6  "F : leadsTo (H i Int HasTok i) (E i)"
    6.11  
     7.1 --- a/src/HOL/UNITY/WFair.thy	Wed Nov 18 11:12:29 1998 +0100
     7.2 +++ b/src/HOL/UNITY/WFair.thy	Wed Nov 18 15:10:46 1998 +0100
     7.3 @@ -15,7 +15,7 @@
     7.4    (*This definition specifies weak fairness.  The rest of the theory
     7.5      is generic to all forms of fairness.*)
     7.6    transient :: "'a set => 'a program set"
     7.7 -    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"
     7.8 +    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
     7.9  
    7.10    ensures :: "['a set, 'a set] => 'a program set"
    7.11      "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
     8.1 --- a/src/HOL/equalities.ML	Wed Nov 18 11:12:29 1998 +0100
     8.2 +++ b/src/HOL/equalities.ML	Wed Nov 18 15:10:46 1998 +0100
     8.3 @@ -336,7 +336,7 @@
     8.4  qed "Un_Diff_Int";
     8.5  
     8.6  
     8.7 -section "Compl";
     8.8 +section "Set complement";
     8.9  
    8.10  Goal "A Int -A = {}";
    8.11  by (Blast_tac 1);