# HG changeset patch
# User haftmann
# Date 1384549325 -3600
# Node ID 82ef58dba83b0d60d23762bb45fab94722fcbf2e
# Parent  0060957404c701e585daeb65e64762a6c25be5ff
dropped duplicate of of_bool

diff -r 0060957404c7 -r 82ef58dba83b src/HOL/ex/Coercion_Examples.thy
--- 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