# HG changeset patch
# User haftmann
# Date 1248265232 -7200
# Node ID ee143615019c0e20ee26e539b483b5da46078eef
# Parent  b513db807fcad2c698212e7e36d0bda338278da7
set intersection and union now named inter and union

diff -r b513db807fca -r ee143615019c NEWS
--- a/NEWS	Wed Jul 22 14:20:31 2009 +0200
+++ b/NEWS	Wed Jul 22 14:20:32 2009 +0200
@@ -18,6 +18,11 @@
 
 *** HOL ***
 
+* More convenient names for set intersection and union.  INCOMPATIBILITY:
+
+    Set.Int ~>  Set.inter
+    Set.Un ~>   Set.union
+
 * Code generator attributes follow the usual underscore convention:
     code_unfold     replaces    code unfold
     code_post       replaces    code post
diff -r b513db807fca -r ee143615019c src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 14:20:31 2009 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 14:20:32 2009 +0200
@@ -648,7 +648,7 @@
            G \<turnstile>Method old member_of superNew
            \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
 
-| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
+| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S intr; G\<turnstile>intr overrides\<^sub>S old\<rbrakk>
              \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
 
 text {* Dynamic overriding (used during the typecheck of the compiler) *}
@@ -668,7 +668,7 @@
            G\<turnstile>resTy new \<preceq> resTy old
            \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
 
-| Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
+| Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
             \<Longrightarrow> G\<turnstile>new overrides old"
 
 syntax
diff -r b513db807fca -r ee143615019c src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Wed Jul 22 14:20:31 2009 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Wed Jul 22 14:20:32 2009 +0200
@@ -161,7 +161,7 @@
 (* assn_tr' & bexp_tr'*)
 ML{*  
 fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_name Set.Int}, _) $ (Const ("Collect",_) $ T1) $ 
+  | assn_tr' (Const (@{const_name inter}, _) $ (Const ("Collect",_) $ T1) $ 
                                    (Const ("Collect",_) $ T2)) =  
             Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
   | assn_tr' t = t;
diff -r b513db807fca -r ee143615019c src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Wed Jul 22 14:20:31 2009 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy	Wed Jul 22 14:20:32 2009 +0200
@@ -163,7 +163,7 @@
 (* assn_tr' & bexp_tr'*)
 ML{*  
 fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_name Int},_) $ (Const ("Collect",_) $ T1) $ 
+  | assn_tr' (Const (@{const_name inter},_) $ (Const ("Collect",_) $ T1) $ 
                                    (Const ("Collect",_) $ T2)) =  
             Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
   | assn_tr' t = t;
diff -r b513db807fca -r ee143615019c src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 14:20:31 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 14:20:32 2009 +0200
@@ -1013,7 +1013,7 @@
               (HOLogic.mk_Trueprop (HOLogic.mk_eq
                 (supp c,
                  if null dts then HOLogic.mk_set atomT []
-                 else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
+                 else foldr1 (HOLogic.mk_binop @{const_name union}) (map supp args2)))))
             (fn _ =>
               simp_tac (HOL_basic_ss addsimps (supp_def ::
                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
diff -r b513db807fca -r ee143615019c src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Jul 22 14:20:31 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Jul 22 14:20:32 2009 +0200
@@ -196,7 +196,7 @@
           | add_set (t, T) ((u, U) :: ps) =
               if T = U then
                 let val S = HOLogic.mk_setT T
-                in (Const (@{const_name "Un"}, S --> S --> S) $ u $ t, T) :: ps
+                in (Const (@{const_name union}, S --> S --> S) $ u $ t, T) :: ps
                 end
               else (u, U) :: add_set (t, T) ps
       in