# HG changeset patch
# User haftmann
# Date 1248183870 -7200
# Node ID a7bc3141e599fb44925e87a0a6adac4377903d0b
# Parent  53a21a5e6889006ce8daf688e3ca46ec506b8e9d
UNIV_code now named UNIV_apply

diff -r 53a21a5e6889 -r a7bc3141e599 src/HOL/NatTransfer.thy
--- 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
 ]