set intersection and union now named inter and union
authorhaftmann
Wed Jul 22 14:20:32 2009 +0200 (2009-07-22)
changeset 32134ee143615019c
parent 32133 b513db807fca
child 32135 f645b51e8e54
set intersection and union now named inter and union
NEWS
src/HOL/Bali/DeclConcepts.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive2.ML
     1.1 --- a/NEWS	Wed Jul 22 14:20:31 2009 +0200
     1.2 +++ b/NEWS	Wed Jul 22 14:20:32 2009 +0200
     1.3 @@ -18,6 +18,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* More convenient names for set intersection and union.  INCOMPATIBILITY:
     1.8 +
     1.9 +    Set.Int ~>  Set.inter
    1.10 +    Set.Un ~>   Set.union
    1.11 +
    1.12  * Code generator attributes follow the usual underscore convention:
    1.13      code_unfold     replaces    code unfold
    1.14      code_post       replaces    code post
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 14:20:31 2009 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 14:20:32 2009 +0200
     2.3 @@ -648,7 +648,7 @@
     2.4             G \<turnstile>Method old member_of superNew
     2.5             \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
     2.6  
     2.7 -| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
     2.8 +| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S intr; G\<turnstile>intr overrides\<^sub>S old\<rbrakk>
     2.9               \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
    2.10  
    2.11  text {* Dynamic overriding (used during the typecheck of the compiler) *}
    2.12 @@ -668,7 +668,7 @@
    2.13             G\<turnstile>resTy new \<preceq> resTy old
    2.14             \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
    2.15  
    2.16 -| Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
    2.17 +| Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
    2.18              \<Longrightarrow> G\<turnstile>new overrides old"
    2.19  
    2.20  syntax
     3.1 --- a/src/HOL/Hoare/Hoare.thy	Wed Jul 22 14:20:31 2009 +0200
     3.2 +++ b/src/HOL/Hoare/Hoare.thy	Wed Jul 22 14:20:32 2009 +0200
     3.3 @@ -161,7 +161,7 @@
     3.4  (* assn_tr' & bexp_tr'*)
     3.5  ML{*  
     3.6  fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
     3.7 -  | assn_tr' (Const (@{const_name Set.Int}, _) $ (Const ("Collect",_) $ T1) $ 
     3.8 +  | assn_tr' (Const (@{const_name inter}, _) $ (Const ("Collect",_) $ T1) $ 
     3.9                                     (Const ("Collect",_) $ T2)) =  
    3.10              Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
    3.11    | assn_tr' t = t;
     4.1 --- a/src/HOL/Hoare/HoareAbort.thy	Wed Jul 22 14:20:31 2009 +0200
     4.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Wed Jul 22 14:20:32 2009 +0200
     4.3 @@ -163,7 +163,7 @@
     4.4  (* assn_tr' & bexp_tr'*)
     4.5  ML{*  
     4.6  fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
     4.7 -  | assn_tr' (Const (@{const_name Int},_) $ (Const ("Collect",_) $ T1) $ 
     4.8 +  | assn_tr' (Const (@{const_name inter},_) $ (Const ("Collect",_) $ T1) $ 
     4.9                                     (Const ("Collect",_) $ T2)) =  
    4.10              Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
    4.11    | assn_tr' t = t;
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 14:20:31 2009 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 14:20:32 2009 +0200
     5.3 @@ -1013,7 +1013,7 @@
     5.4                (HOLogic.mk_Trueprop (HOLogic.mk_eq
     5.5                  (supp c,
     5.6                   if null dts then HOLogic.mk_set atomT []
     5.7 -                 else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
     5.8 +                 else foldr1 (HOLogic.mk_binop @{const_name union}) (map supp args2)))))
     5.9              (fn _ =>
    5.10                simp_tac (HOL_basic_ss addsimps (supp_def ::
    5.11                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
     6.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Jul 22 14:20:31 2009 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Jul 22 14:20:32 2009 +0200
     6.3 @@ -196,7 +196,7 @@
     6.4            | add_set (t, T) ((u, U) :: ps) =
     6.5                if T = U then
     6.6                  let val S = HOLogic.mk_setT T
     6.7 -                in (Const (@{const_name "Un"}, S --> S --> S) $ u $ t, T) :: ps
     6.8 +                in (Const (@{const_name union}, S --> S --> S) $ u $ t, T) :: ps
     6.9                  end
    6.10                else (u, U) :: add_set (t, T) ps
    6.11        in