HOL += HOL-Complex
authorhaftmann
Tue Jul 01 07:58:17 2008 +0200 (2008-07-01)
changeset 274217e458bd56860
parent 27420 aa335405f0c5
child 27422 73d25d422124
HOL += HOL-Complex
NEWS
src/HOL/Complex/ROOT.ML
src/HOL/Complex/ex/ROOT.ML
src/HOL/Complex/ex/document/root.tex
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/ex/ExecutableContent.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/NEWS	Tue Jul 01 07:13:45 2008 +0200
     1.2 +++ b/NEWS	Tue Jul 01 07:58:17 2008 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Integrated image HOL-Complex with HOL.
     1.8 +
     1.9  * Methods "case_tac" and "induct_tac" now refer to the very same rules
    1.10  as the structured Isar versions "cases" and "induct", cf. the
    1.11  corresponding "cases" and "induct" attributes.  Mutual induction rules
     2.1 --- a/src/HOL/Complex/ROOT.ML	Tue Jul 01 07:13:45 2008 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,8 +0,0 @@
     2.4 -(*  Title:      HOL/Complex/ROOT.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Jacques Fleuriot
     2.7 -
     2.8 -The Complex Numbers.
     2.9 -*)
    2.10 -
    2.11 -use_thy "Complex_Main";
     3.1 --- a/src/HOL/Complex/ex/ROOT.ML	Tue Jul 01 07:13:45 2008 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,28 +0,0 @@
     3.4 -(*  Title:      HOL/Complex/ex/ROOT.ML
     3.5 -    ID:         $Id$
     3.6 -
     3.7 -Miscellaneous examples.
     3.8 -*)
     3.9 -
    3.10 -no_document use_thys [
    3.11 -  "../../NumberTheory/Factorization",
    3.12 -  "BigO",
    3.13 -  "NatPair"
    3.14 -];
    3.15 -
    3.16 -use_thys [
    3.17 -  "BinEx",
    3.18 -  "Sqrt",
    3.19 -  "Sqrt_Script",
    3.20 -  "NSPrimes",
    3.21 -  "BigO_Complex",
    3.22 -
    3.23 -  "Arithmetic_Series_Complex",
    3.24 -  "HarmonicSeries",
    3.25 -
    3.26 -  "DenumRat",
    3.27 -  
    3.28 -  "MIR",
    3.29 -  "ReflectedFerrack"
    3.30 -];
    3.31 -
     4.1 --- a/src/HOL/Complex/ex/document/root.tex	Tue Jul 01 07:13:45 2008 +0200
     4.2 +++ b/src/HOL/Complex/ex/document/root.tex	Tue Jul 01 07:58:17 2008 +0200
     4.3 @@ -1,20 +0,0 @@
     4.4 -
     4.5 -\documentclass[11pt,a4paper]{article}
     4.6 -\usepackage[latin1]{inputenc}
     4.7 -\usepackage{isabelle,isabellesym}
     4.8 -\usepackage{pdfsetup}
     4.9 -
    4.10 -\urlstyle{rm}
    4.11 -\isabellestyle{it}
    4.12 -
    4.13 -\begin{document}
    4.14 -
    4.15 -\title{Miscellaneous HOL-Complex Examples}
    4.16 -\maketitle
    4.17 -
    4.18 -\tableofcontents
    4.19 -
    4.20 -\parindent 0pt\parskip 0.5ex
    4.21 -\input{session}
    4.22 -
    4.23 -\end{document}
     5.1 --- a/src/HOL/IsaMakefile	Tue Jul 01 07:13:45 2008 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Tue Jul 01 07:58:17 2008 +0200
     5.3 @@ -5,9 +5,8 @@
     5.4  ## targets
     5.5  
     5.6  default: HOL
     5.7 -generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
     5.8 -images: HOL-Plain HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
     5.9 -        HOL-Word TLA HOL4
    5.10 +generate: HOL-Generate-HOL HOL-Generate-HOLLight
    5.11 +images: HOL-Plain HOL HOL-Algebra HOL-Nominal HOL-Word TLA HOL4
    5.12  
    5.13  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    5.14  test: \
    5.15 @@ -16,12 +15,11 @@
    5.16    HOL-Auth \
    5.17    HOL-AxClasses \
    5.18    HOL-Bali \
    5.19 -  HOL-Complex-HahnBanach \
    5.20 -  HOL-Complex-Import \
    5.21 -  HOL-Complex-ex \
    5.22    HOL-Extraction \
    5.23 +  HOL-HahnBanach \
    5.24    HOL-Hoare \
    5.25    HOL-HoareParallel \
    5.26 +  HOL-Import \
    5.27    HOL-IMP \
    5.28    HOL-IMPP \
    5.29    HOL-IOA \
    5.30 @@ -179,97 +177,19 @@
    5.31  
    5.32  $(OUT)/HOL: $(OUT)/HOL-Plain \
    5.33    ROOT.ML \
    5.34 +  Arith_Tools.thy \
    5.35    ATP_Linkup.thy \
    5.36 -  Arith_Tools.thy \
    5.37 +  Complex/CLim.thy \
    5.38 +  Complex/Complex_Main.thy \
    5.39 +  Complex/Complex.thy \
    5.40 +  Complex/CStar.thy \
    5.41 +  Complex/Fundamental_Theorem_Algebra.thy \
    5.42 +  Complex/NSCA.thy \
    5.43 +  Complex/NSComplex.thy \
    5.44 +  Complex/ROOT.ML \
    5.45    Equiv_Relations.thy \
    5.46    Groebner_Basis.thy \
    5.47    Hilbert_Choice.thy \
    5.48 -  Int.thy \
    5.49 -  IntDiv.thy \
    5.50 -  List.thy \
    5.51 -  Main.thy \
    5.52 -  Map.thy \
    5.53 -  NatBin.thy \
    5.54 -  Presburger.thy \
    5.55 -  Recdef.thy \
    5.56 -  Relation_Power.thy \
    5.57 -  SetInterval.thy \
    5.58 -  Tools/Groebner_Basis/groebner.ML \
    5.59 -  Tools/Groebner_Basis/misc.ML \
    5.60 -  Tools/Groebner_Basis/normalizer.ML \
    5.61 -  Tools/Groebner_Basis/normalizer_data.ML \
    5.62 -  Tools/Qelim/cooper.ML \
    5.63 -  Tools/Qelim/cooper_data.ML \
    5.64 -  Tools/Qelim/generated_cooper.ML \
    5.65 -  Tools/Qelim/presburger.ML \
    5.66 -  Tools/Qelim/qelim.ML \
    5.67 -  Tools/TFL/casesplit.ML \
    5.68 -  Tools/TFL/dcterm.ML \
    5.69 -  Tools/TFL/post.ML \
    5.70 -  Tools/TFL/rules.ML \
    5.71 -  Tools/TFL/tfl.ML \
    5.72 -  Tools/TFL/thms.ML \
    5.73 -  Tools/TFL/thry.ML \
    5.74 -  Tools/TFL/usyntax.ML \
    5.75 -  Tools/TFL/utils.ML \
    5.76 -  Tools/meson.ML \
    5.77 -  Tools/metis_tools.ML \
    5.78 -  Tools/numeral.ML \
    5.79 -  Tools/numeral_syntax.ML \
    5.80 -  Tools/polyhash.ML \
    5.81 -  Tools/recdef_package.ML \
    5.82 -  Tools/res_atp.ML \
    5.83 -  Tools/res_atp_methods.ML \
    5.84 -  Tools/res_atp_provers.ML \
    5.85 -  Tools/res_axioms.ML \
    5.86 -  Tools/res_clause.ML \
    5.87 -  Tools/res_hol_clause.ML \
    5.88 -  Tools/res_reconstruct.ML \
    5.89 -  Tools/specification_package.ML \
    5.90 -  Tools/string_syntax.ML \
    5.91 -  Tools/watcher.ML \
    5.92 -  int_arith1.ML \
    5.93 -  int_factor_simprocs.ML \
    5.94 -  nat_simprocs.ML \
    5.95 -  $(SRC)/Provers/Arith/assoc_fold.ML \
    5.96 -  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
    5.97 -  $(SRC)/Provers/Arith/cancel_numerals.ML \
    5.98 -  $(SRC)/Provers/Arith/combine_numerals.ML \
    5.99 -  $(SRC)/Provers/Arith/extract_common_term.ML \
   5.100 -  $(SRC)/Tools/Metis/metis.ML
   5.101 -	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL-Plain HOL
   5.102 -
   5.103 -
   5.104 -## HOL-Complex-HahnBanach
   5.105 -
   5.106 -HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
   5.107 -
   5.108 -$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex			\
   5.109 -  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
   5.110 -  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
   5.111 -  Real/HahnBanach/HahnBanachExtLemmas.thy				\
   5.112 -  Real/HahnBanach/HahnBanachSupLemmas.thy				\
   5.113 -  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy	\
   5.114 -  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML			\
   5.115 -  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
   5.116 -  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
   5.117 -  Real/HahnBanach/document/root.tex
   5.118 -	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
   5.119 -
   5.120 -
   5.121 -## HOL-Complex
   5.122 -
   5.123 -HOL-Complex: HOL $(OUT)/HOL-Complex
   5.124 -
   5.125 -$(OUT)/HOL-Complex: $(OUT)/HOL \
   5.126 -  Complex/ROOT.ML \
   5.127 -  Complex/CLim.thy \
   5.128 -  Complex/CStar.thy \
   5.129 -  Complex/Complex.thy \
   5.130 -  Complex/Complex_Main.thy \
   5.131 -  Complex/Fundamental_Theorem_Algebra.thy \
   5.132 -  Complex/NSCA.thy \
   5.133 -  Complex/NSComplex.thy \
   5.134    Hyperreal/Deriv.thy \
   5.135    Hyperreal/Fact.thy \
   5.136    Hyperreal/Filter.thy \
   5.137 @@ -282,22 +202,26 @@
   5.138    Hyperreal/HyperDef.thy \
   5.139    Hyperreal/HyperNat.thy \
   5.140    Hyperreal/Hyperreal.thy \
   5.141 +  Hyperreal/hypreal_arith.ML \
   5.142    Hyperreal/Integration.thy \
   5.143    Hyperreal/Lim.thy \
   5.144    Hyperreal/Ln.thy \
   5.145    Hyperreal/Log.thy \
   5.146    Hyperreal/MacLaurin.thy \
   5.147 +  Hyperreal/NatStar.thy \
   5.148    Hyperreal/NSA.thy \
   5.149 -  Hyperreal/NatStar.thy \
   5.150    Hyperreal/NthRoot.thy \
   5.151    Hyperreal/SEQ.thy \
   5.152    Hyperreal/Series.thy \
   5.153 +  Hyperreal/StarDef.thy \
   5.154    Hyperreal/Star.thy \
   5.155 -  Hyperreal/StarDef.thy \
   5.156    Hyperreal/Taylor.thy \
   5.157    Hyperreal/Transcendental.thy \
   5.158 -  Hyperreal/hypreal_arith.ML \
   5.159    Hyperreal/transfer.ML \
   5.160 +  int_arith1.ML \
   5.161 +  IntDiv.thy \
   5.162 +  int_factor_simprocs.ML \
   5.163 +  Int.thy \
   5.164    Library/Abstract_Rat.thy \
   5.165    Library/Dense_Linear_Order.thy \
   5.166    Library/GCD.thy \
   5.167 @@ -306,36 +230,71 @@
   5.168    Library/Parity.thy \
   5.169    Library/Univ_Poly.thy \
   5.170    Library/Zorn.thy \
   5.171 +  List.thy \
   5.172 +  Main.thy \
   5.173 +  Map.thy \
   5.174 +  NatBin.thy \
   5.175 +  nat_simprocs.ML \
   5.176 +  Presburger.thy \
   5.177    Real/ContNotDenum.thy \
   5.178    Real/Lubs.thy \
   5.179    Real/PReal.thy \
   5.180 -  Real/RComplete.thy \
   5.181 +  Real/rat_arith.ML \
   5.182    Real/Rational.thy \
   5.183 -  Real/Real.thy \
   5.184 +  Real/RComplete.thy \
   5.185 +  Real/real_arith.ML \
   5.186    Real/RealDef.thy \
   5.187    Real/RealPow.thy \
   5.188 +  Real/Real.thy \
   5.189    Real/RealVector.thy \
   5.190 -  Real/rat_arith.ML \
   5.191 -  Real/real_arith.ML \
   5.192 +  Recdef.thy \
   5.193 +  Relation_Power.thy \
   5.194 +  SetInterval.thy \
   5.195 +  $(SRC)/Provers/Arith/assoc_fold.ML \
   5.196 +  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
   5.197 +  $(SRC)/Provers/Arith/cancel_numerals.ML \
   5.198 +  $(SRC)/Provers/Arith/combine_numerals.ML \
   5.199 +  $(SRC)/Provers/Arith/extract_common_term.ML \
   5.200 +  $(SRC)/Tools/Metis/metis.ML \
   5.201 +  Tools/Groebner_Basis/groebner.ML \
   5.202 +  Tools/Groebner_Basis/misc.ML \
   5.203 +  Tools/Groebner_Basis/normalizer_data.ML \
   5.204 +  Tools/Groebner_Basis/normalizer.ML \
   5.205 +  Tools/meson.ML \
   5.206 +  Tools/metis_tools.ML \
   5.207 +  Tools/numeral.ML \
   5.208 +  Tools/numeral_syntax.ML \
   5.209 +  Tools/polyhash.ML \
   5.210 +  Tools/Qelim/cooper_data.ML \
   5.211 +  Tools/Qelim/cooper.ML \
   5.212 +  Tools/Qelim/ferrante_rackoff_data.ML \
   5.213    Tools/Qelim/ferrante_rackoff.ML \
   5.214 -  Tools/Qelim/ferrante_rackoff_data.ML \
   5.215 +  Tools/Qelim/generated_cooper.ML \
   5.216 +  Tools/Qelim/langford_data.ML \
   5.217    Tools/Qelim/langford.ML \
   5.218 -  Tools/Qelim/langford_data.ML
   5.219 -	@cd Complex; $(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL HOL-Complex
   5.220 -
   5.221 -
   5.222 -## HOL-Complex-ex
   5.223 -
   5.224 -HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
   5.225 -
   5.226 -$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy		\
   5.227 -  Complex/ex/ROOT.ML Complex/ex/document/root.tex			\
   5.228 -  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy			\
   5.229 -  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy				\
   5.230 -  Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
   5.231 -  Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy			\
   5.232 -  Complex/ex/linreif.ML Complex/ex/linrtac.ML
   5.233 -	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
   5.234 +  Tools/Qelim/presburger.ML \
   5.235 +  Tools/Qelim/qelim.ML \
   5.236 +  Tools/recdef_package.ML \
   5.237 +  Tools/res_atp_methods.ML \
   5.238 +  Tools/res_atp.ML \
   5.239 +  Tools/res_atp_provers.ML \
   5.240 +  Tools/res_axioms.ML \
   5.241 +  Tools/res_clause.ML \
   5.242 +  Tools/res_hol_clause.ML \
   5.243 +  Tools/res_reconstruct.ML \
   5.244 +  Tools/specification_package.ML \
   5.245 +  Tools/string_syntax.ML \
   5.246 +  Tools/TFL/casesplit.ML \
   5.247 +  Tools/TFL/dcterm.ML \
   5.248 +  Tools/TFL/post.ML \
   5.249 +  Tools/TFL/rules.ML \
   5.250 +  Tools/TFL/tfl.ML \
   5.251 +  Tools/TFL/thms.ML \
   5.252 +  Tools/TFL/thry.ML \
   5.253 +  Tools/TFL/usyntax.ML \
   5.254 +  Tools/TFL/utils.ML \
   5.255 +  Tools/watcher.ML
   5.256 +	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL-Plain HOL
   5.257  
   5.258  
   5.259  ## HOL-Library
   5.260 @@ -371,6 +330,23 @@
   5.261  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
   5.262  
   5.263  
   5.264 +## HOL-HahnBanach
   5.265 +
   5.266 +HOL-HahnBanach: HOL $(LOG)/HOL-HahnBanach.gz
   5.267 +
   5.268 +$(LOG)/HOL-HahnBanach.gz: $(OUT)/HOL			\
   5.269 +  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
   5.270 +  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
   5.271 +  Real/HahnBanach/HahnBanachExtLemmas.thy				\
   5.272 +  Real/HahnBanach/HahnBanachSupLemmas.thy				\
   5.273 +  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy	\
   5.274 +  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML			\
   5.275 +  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
   5.276 +  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
   5.277 +  Real/HahnBanach/document/root.tex
   5.278 +	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL HahnBanach
   5.279 +
   5.280 +
   5.281  ## HOL-Subst
   5.282  
   5.283  HOL-Subst: HOL $(LOG)/HOL-Subst.gz
   5.284 @@ -413,7 +389,7 @@
   5.285  	@$(ISATOOL) usedir $(OUT)/HOL IMPP
   5.286  
   5.287  
   5.288 -## HOL-Complex-Import
   5.289 +## HOL-Import
   5.290  
   5.291  IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
   5.292    Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
   5.293 @@ -425,38 +401,38 @@
   5.294    Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
   5.295    Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
   5.296  
   5.297 -HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz
   5.298 +HOL-Import: HOL $(LOG)/HOL-Import.gz
   5.299  
   5.300 -$(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)
   5.301 -	@$(ISATOOL) usedir $(OUT)/HOL-Complex Import
   5.302 +$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
   5.303 +	@$(ISATOOL) usedir $(OUT)/HOL Import
   5.304  
   5.305  
   5.306 -## HOL-Complex-Generate-HOL
   5.307 +## HOL-Generate-HOL
   5.308  
   5.309 -HOL-Complex-Generate-HOL: HOL-Complex $(LOG)/HOL-Complex-Generate-HOL.gz
   5.310 +HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz
   5.311  
   5.312 -$(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex			\
   5.313 +$(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL			\
   5.314    $(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy			\
   5.315    Import/Generate-HOL/GenHOL4Prob.thy					\
   5.316    Import/Generate-HOL/GenHOL4Real.thy					\
   5.317    Import/Generate-HOL/GenHOL4Vec.thy					\
   5.318    Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
   5.319 -	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL
   5.320 +	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOL
   5.321  
   5.322  
   5.323 -## HOL-Complex-Generate-HOLLight
   5.324 +## HOL-Generate-HOLLight
   5.325  
   5.326 -HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz
   5.327 +HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
   5.328  
   5.329 -$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex		\
   5.330 +$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL		\
   5.331    $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy	\
   5.332    Import/Generate-HOLLight/ROOT.ML
   5.333 -	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight
   5.334 +	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOLLight
   5.335  
   5.336  
   5.337  ## HOL-Import-HOL
   5.338  
   5.339 -HOL4: HOL-Complex $(LOG)/HOL4.gz
   5.340 +HOL4: HOL $(LOG)/HOL4.gz
   5.341  
   5.342  HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
   5.343    bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
   5.344 @@ -469,19 +445,19 @@
   5.345    seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
   5.346    word_base.imp word_bitop.imp word_num.imp
   5.347  
   5.348 -$(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)			\
   5.349 +$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES)			\
   5.350    $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy		\
   5.351    Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy			\
   5.352    Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy	\
   5.353    Import/HOL/ROOT.ML
   5.354 -	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4
   5.355 +	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL HOL4
   5.356  
   5.357 -HOLLight: HOL-Complex $(LOG)/HOLLight.gz
   5.358 +HOLLight: HOL $(LOG)/HOLLight.gz
   5.359  
   5.360 -$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES)	\
   5.361 +$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES)	\
   5.362    Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy		\
   5.363    Import/HOLLight/ROOT.ML
   5.364 -	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOLLight
   5.365 +	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL HOLLight
   5.366  
   5.367  
   5.368  ## HOL-NumberTheory
   5.369 @@ -790,6 +766,7 @@
   5.370  HOL-ex: HOL $(LOG)/HOL-ex.gz
   5.371  
   5.372  $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy		\
   5.373 +  Library/Primes.thy							\
   5.374    ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy	\
   5.375    ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
   5.376    ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy			\
   5.377 @@ -810,7 +787,12 @@
   5.378    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   5.379    ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib	\
   5.380    ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
   5.381 -  ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
   5.382 +  ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy	\
   5.383 +  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy			\
   5.384 +  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy				\
   5.385 +  Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
   5.386 +  Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy			\
   5.387 +  Complex/ex/linreif.ML Complex/ex/linrtac.ML
   5.388  	@$(ISATOOL) usedir $(OUT)/HOL ex
   5.389  
   5.390  
   5.391 @@ -844,11 +826,11 @@
   5.392  	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
   5.393  
   5.394  
   5.395 -## HOL-Complex-Matrix
   5.396 +## HOL-Matrix
   5.397  
   5.398 -HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
   5.399 +HOL-Matrix: HOL $(OUT)/HOL-Matrix
   5.400  
   5.401 -$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex				\
   5.402 +$(OUT)/HOL-Matrix: $(OUT)/HOL				\
   5.403    $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy			\
   5.404    $(SRC)/Tools/Compute_Oracle/am_compiler.ML				\
   5.405    $(SRC)/Tools/Compute_Oracle/am_interpreter.ML				\
   5.406 @@ -863,7 +845,7 @@
   5.407    Matrix/cplex/FloatSparseMatrix.thy					\
   5.408    Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML	\
   5.409    Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML
   5.410 -	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
   5.411 +	@$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
   5.412  
   5.413  
   5.414  ## TLA
   5.415 @@ -986,7 +968,7 @@
   5.416  ## clean
   5.417  
   5.418  clean:
   5.419 -	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
   5.420 +	@rm -f  $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
   5.421  		$(LOG)/HOL.gz $(LOG)/TLA.gz \
   5.422  		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
   5.423  		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
   5.424 @@ -999,9 +981,7 @@
   5.425  		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
   5.426                  $(LOG)/HOL-Nominal-Examples.gz \
   5.427  		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
   5.428 -		$(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
   5.429 -		$(LOG)/HOL-Complex.gz \
   5.430 -		$(LOG)/HOL-Complex-ex.gz \
   5.431 -		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
   5.432 +		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
   5.433 +		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
   5.434                  $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
   5.435  		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz 
     6.1 --- a/src/HOL/ROOT.ML	Tue Jul 01 07:13:45 2008 +0200
     6.2 +++ b/src/HOL/ROOT.ML	Tue Jul 01 07:58:17 2008 +0200
     6.3 @@ -4,4 +4,4 @@
     6.4  Classical Higher-order Logic -- batteries included.
     6.5  *)
     6.6  
     6.7 -use_thy "Main";
     6.8 +use_thy "Complex/Complex_Main";
     7.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue Jul 01 07:13:45 2008 +0200
     7.2 +++ b/src/HOL/ex/ExecutableContent.thy	Tue Jul 01 07:58:17 2008 +0200
     7.3 @@ -6,17 +6,12 @@
     7.4  
     7.5  theory ExecutableContent
     7.6  imports
     7.7 -  Main
     7.8 -  Eval
     7.9 -  Enum
    7.10 -  Code_Index
    7.11 -  "~~/src/HOL/ex/Records"
    7.12 +  Complex_Main
    7.13    AssocList
    7.14    Binomial
    7.15    Commutative_Ring
    7.16 -  "~~/src/HOL/ex/Commutative_Ring_Complete"
    7.17 -  "~~/src/HOL/Real/RealDef"
    7.18 -  GCD
    7.19 +  Enum
    7.20 +  Eval
    7.21    List_Prefix
    7.22    Nat_Infinity
    7.23    NatPair
    7.24 @@ -29,11 +24,73 @@
    7.25    State_Monad
    7.26    While_Combinator
    7.27    Word
    7.28 +  "~~/src/HOL/ex/Commutative_Ring_Complete"
    7.29 +  "~~/src/HOL/ex/Records"
    7.30  begin
    7.31  
    7.32  lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
    7.33  declare fast_bv_to_nat_helper.simps [code func del]
    7.34  
    7.35 +(*FIXME distribute to theories*)
    7.36 +declare divides_def [code func del] -- "Univ_Poly"
    7.37 +declare unstar_def [code func del] -- "StarDef"
    7.38 +declare star_one_def [code func del] -- "StarDef"
    7.39 +declare star_mult_def [code func del] -- "StarDef"
    7.40 +declare star_add_def [code func del] -- "StarDef"
    7.41 +declare star_zero_def [code func del] -- "StarDef"
    7.42 +declare star_minus_def [code func del] -- "StarDef"
    7.43 +declare star_diff_def [code func del] -- "StarDef"
    7.44 +declare Reals_def [code func del] -- "RealVector"
    7.45 +declare star_scaleR_def [code func del] -- "HyperDef"
    7.46 +declare hyperpow_def [code func del] -- HyperDef
    7.47 +declare Infinitesimal_def [code func del] -- NSA
    7.48 +declare HFinite_def [code func del] -- NSA
    7.49 +declare floor_def [code func del] -- RComplete
    7.50 +declare LIMSEQ_def [code func del] -- SEQ
    7.51 +declare partition_def [code func del] -- Integration
    7.52 +declare Integral_def [code func del] -- Integration
    7.53 +declare tpart_def [code func del] -- Integration
    7.54 +declare psize_def [code func del] -- Integration
    7.55 +declare gauge_def [code func del] -- Integration
    7.56 +declare fine_def [code func del] -- Integration
    7.57 +declare sumhr_def [code func del] -- HSeries
    7.58 +declare NSsummable_def [code func del] -- HSeries
    7.59 +declare NSLIMSEQ_def [code func del] -- HSEQ
    7.60 +declare newInt.simps [code func del] -- ContNotDenum
    7.61 +declare LIM_def [code func del] -- Lim
    7.62 +declare NSLIM_def [code func del] -- HLim
    7.63 +declare HComplex_def [code func del]
    7.64 +declare of_hypnat_def [code func del]
    7.65 +declare InternalSets_def [code func del]
    7.66 +declare InternalFuns_def [code func del]
    7.67 +declare increment_def [code func del]
    7.68 +declare is_starext_def [code func del]
    7.69 +declare hrcis_def [code func del]
    7.70 +declare hexpi_def [code func del]
    7.71 +declare hsgn_def [code func del]
    7.72 +declare hcnj_def [code func del]
    7.73 +declare hcis_def [code func del]
    7.74 +declare harg_def [code func del]
    7.75 +declare isNSUCont_def [code func del]
    7.76 +declare hRe_def [code func del]
    7.77 +declare hIm_def [code func del]
    7.78 +declare HInfinite_def [code func del]
    7.79 +declare hSuc_def [code func del]
    7.80 +declare NSCauchy_def [code func del]
    7.81 +declare of_hypreal_def [code func del]
    7.82 +declare isNSCont_def [code func del]
    7.83 +declare monoseq_def [code func del]
    7.84 +declare scaleHR_def [code func del]
    7.85 +declare isUCont_def [code func del]
    7.86 +declare NSBseq_def [code func del]
    7.87 +declare subseq_def [code func del]
    7.88 +declare Cauchy_def [code func del]
    7.89 +declare powhr_def [code func del]
    7.90 +declare hlog_def [code func del]
    7.91 +declare Zseq_def [code func del]
    7.92 +declare Bseq_def [code func del]
    7.93 +declare stc_def [code func del]
    7.94 +
    7.95  setup {*
    7.96    Code.del_funcs
    7.97      (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))
     8.1 --- a/src/HOL/ex/ROOT.ML	Tue Jul 01 07:13:45 2008 +0200
     8.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jul 01 07:58:17 2008 +0200
     8.3 @@ -87,3 +87,25 @@
     8.4  
     8.5  HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
     8.6  
     8.7 +no_document use_thys [
     8.8 +  "../NumberTheory/Factorization",
     8.9 +  "../Library/BigO",
    8.10 +  "../Library/NatPair"
    8.11 +];
    8.12 +
    8.13 +use_thys [
    8.14 +  "../Complex/ex/BinEx",
    8.15 +  "../Complex/ex/Sqrt",
    8.16 +  "../Complex/ex/Sqrt_Script",
    8.17 +  "../Complex/ex/NSPrimes",
    8.18 +  "../Complex/ex/BigO_Complex",
    8.19 +
    8.20 +  "../Complex/ex/Arithmetic_Series_Complex",
    8.21 +  "../Complex/ex/HarmonicSeries",
    8.22 +
    8.23 +  "../Complex/ex/DenumRat",
    8.24 +  
    8.25 +  "../Complex/ex/MIR",
    8.26 +  "../Complex/ex/ReflectedFerrack"
    8.27 +];
    8.28 +