# HG changeset patch
# User wenzelm
# Date 1310131108 -7200
# Node ID 8a61f2441b62e452f249be428e55cc38fe181c21
# Parent  4068e95f1e43ad9d2dab974fcad8b628518cc11c# Parent  c37a1f29bbc07aff7adbf9dfa88599fa1d925e1f
merged

diff -r c37a1f29bbc0 -r 8a61f2441b62 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Jul 08 15:17:40 2011 +0200
+++ b/src/HOL/Archimedean_Field.thy	Fri Jul 08 15:18:28 2011 +0200
@@ -143,7 +143,7 @@
 
 definition
   floor :: "'a::archimedean_field \<Rightarrow> int" where
-  "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+  [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
 
 notation (xsymbols)
   floor  ("\<lfloor>_\<rfloor>")
@@ -274,7 +274,7 @@
 
 definition
   ceiling :: "'a::archimedean_field \<Rightarrow> int" where
-  "ceiling x = - floor (- x)"
+  [code del]: "ceiling x = - floor (- x)"
 
 notation (xsymbols)
   ceiling  ("\<lceil>_\<rceil>")
diff -r c37a1f29bbc0 -r 8a61f2441b62 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Jul 08 15:17:40 2011 +0200
+++ b/src/HOL/Fun.thy	Fri Jul 08 15:18:28 2011 +0200
@@ -148,6 +148,10 @@
 abbreviation
   "bij f \<equiv> bij_betw f UNIV UNIV"
 
+text{* The negated case: *}
+translations
+"\<not> CONST surj f" <= "CONST range f \<noteq> CONST UNIV"
+
 lemma injI:
   assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
   shows "inj f"