--- 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>")
--- 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"