src/HOL/ex/Coercion_Examples.thy
changeset 51247 064683ba110c
parent 40839 48e01d16dd17
child 51320 c1cb872ccb2b
--- a/src/HOL/ex/Coercion_Examples.thy	Fri Feb 22 13:36:31 2013 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy	Fri Feb 22 13:38:10 2013 +0100
@@ -5,9 +5,11 @@
 *)
 
 theory Coercion_Examples
-imports Complex_Main
+imports Main
 begin
 
+declare[[coercion_enabled]]
+
 (* Error messages test *)
 
 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"