# HG changeset patch
# User traytel
# Date 1361536690 -3600
# Node ID 064683ba110c70880345c867f7d1d19edd1ca1c6
# Parent  755562fd2d9d329c89dda893785533a4370cfd5a
Coercion_Examples defines required coercions itself (no Complex_Main needed)

diff -r 755562fd2d9d -r 064683ba110c src/HOL/ex/Coercion_Examples.thy
--- 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"