# HG changeset patch
# User wenzelm
# Date 1291199544 -3600
# Node ID 48e01d16dd176d29d40e50f3c869036e4fe1991d
# Parent  d9bd6df700a8122af86f7ad6bf0b2f9175a3d470
activate subtyping/coercions in theory Complex_Main;

diff -r d9bd6df700a8 -r 48e01d16dd17 src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Wed Dec 01 11:06:01 2010 +0100
+++ b/src/HOL/Complex_Main.thy	Wed Dec 01 11:32:24 2010 +0100
@@ -10,6 +10,9 @@
   Ln
   Taylor
   Deriv
+uses "~~/src/Tools/subtyping.ML"
 begin
 
+setup Subtyping.setup
+
 end
diff -r d9bd6df700a8 -r 48e01d16dd17 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Dec 01 11:06:01 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 01 11:32:24 2010 +0100
@@ -385,6 +385,7 @@
 	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
 
 HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
+  $(SRC)/Tools/subtyping.ML \
   Archimedean_Field.thy \
   Complex.thy \
   Complex_Main.thy \
@@ -408,9 +409,9 @@
   Series.thy \
   SupInf.thy \
   Taylor.thy \
-  Transcendental.thy \
+  Tools/SMT/smt_real.ML \
   Tools/float_syntax.ML \
-  Tools/SMT/smt_real.ML
+  Transcendental.thy
 
 $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
 	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
@@ -1049,7 +1050,7 @@
   ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy	\
   ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy	\
   ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML	\
-  ex/svc_test.thy $(SRC)/Tools/subtyping.ML
+  ex/svc_test.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
 
diff -r d9bd6df700a8 -r 48e01d16dd17 src/HOL/ex/Coercion_Examples.thy
--- a/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 11:06:01 2010 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 11:32:24 2010 +0100
@@ -5,12 +5,9 @@
 *)
 
 theory Coercion_Examples
-imports Main
-uses "~~/src/Tools/subtyping.ML"
+imports Complex_Main
 begin
 
-setup Subtyping.setup
-
 (* Error messages test *)
 
 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"