--- a/src/HOL/NatTransfer.thy Tue Jul 21 14:38:07 2009 +0200
+++ b/src/HOL/NatTransfer.thy Tue Jul 21 15:44:30 2009 +0200
@@ -380,12 +380,16 @@
"(even (int x)) = (even x)"
by (auto simp add: zdvd_int even_nat_def)
+lemma UNIV_apply:
+ "UNIV x = True"
+ by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq)
+
declare TransferMorphism_int_nat[transfer add return:
transfer_int_nat_numerals
transfer_int_nat_functions
transfer_int_nat_function_closures
transfer_int_nat_relations
- UNIV_code
+ UNIV_apply
]