changeset 32264 | 0be31453f698 |
parent 32121 | a7bc3141e599 |
child 32554 | 4ccd84fb19d3 |
--- a/src/HOL/NatTransfer.thy Tue Jul 28 13:37:08 2009 +0200 +++ b/src/HOL/NatTransfer.thy Tue Jul 28 13:37:09 2009 +0200 @@ -382,7 +382,7 @@ lemma UNIV_apply: "UNIV x = True" - by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq) + by (simp add: top_fun_eq top_bool_eq) declare TransferMorphism_int_nat[transfer add return: transfer_int_nat_numerals