--- a/src/HOL/ex/Coercion_Examples.thy Fri Nov 15 22:02:01 2013 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy Fri Nov 15 22:02:05 2013 +0100
@@ -37,10 +37,9 @@
(* Coercion/type maps definitions *)
-primrec nat_of_bool :: "bool \<Rightarrow> nat"
+abbreviation nat_of_bool :: "bool \<Rightarrow> nat"
where
- "nat_of_bool False = 0"
-| "nat_of_bool True = 1"
+ "nat_of_bool \<equiv> of_bool"
declare [[coercion nat_of_bool]]
@@ -201,5 +200,5 @@
declare [[coercion_args uminus -]]
declare [[coercion_args plus + +]]
term "- (n + m)"
-
+
end