src/HOL/Code_Numeral.thy

 imports Nat_Transfer Divides Lifting
 begin
 
 subsection \<open>Type of target language integers\<close>
 
-typedef integer = "UNIV \<Colon> int set"
+typedef integer = "UNIV :: int set"
   morphisms int_of_integer integer_of_int ..
 
 setup_lifting type_definition_integer
 
 lemma integer_eq_iff:

   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 
 subsection \<open>Type of target language naturals\<close>
 
-typedef natural = "UNIV \<Colon> nat set"
+typedef natural = "UNIV :: nat set"
   morphisms nat_of_natural natural_of_nat ..
 
 setup_lifting type_definition_natural
 
 lemma natural_eq_iff [termination_simp]: