src/HOL/Set.thy
changeset 18851 9502ce541f01
parent 18832 6ab4de872a70
child 19175 c6e4b073f6a5
     1.1 --- a/src/HOL/Set.thy	Mon Jan 30 08:20:06 2006 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Jan 30 08:20:56 2006 +0100
     1.3 @@ -2244,4 +2244,10 @@
     1.4    ord_eq_less_trans
     1.5    trans
     1.6  
     1.7 +subsection {* Code generator setup *}
     1.8 +
     1.9 +code_alias
    1.10 +  "op Int" "Set.inter"
    1.11 +  "op Un" "Set.union"
    1.12 +
    1.13  end