--- a/NEWS Tue Jul 01 07:13:45 2008 +0200
+++ b/NEWS Tue Jul 01 07:58:17 2008 +0200
@@ -28,6 +28,8 @@
*** HOL ***
+* Integrated image HOL-Complex with HOL.
+
* Methods "case_tac" and "induct_tac" now refer to the very same rules
as the structured Isar versions "cases" and "induct", cf. the
corresponding "cases" and "induct" attributes. Mutual induction rules
--- a/src/HOL/Complex/ROOT.ML Tue Jul 01 07:13:45 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(* Title: HOL/Complex/ROOT.ML
- ID: $Id$
- Author: Jacques Fleuriot
-
-The Complex Numbers.
-*)
-
-use_thy "Complex_Main";
--- a/src/HOL/Complex/ex/ROOT.ML Tue Jul 01 07:13:45 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/Complex/ex/ROOT.ML
- ID: $Id$
-
-Miscellaneous examples.
-*)
-
-no_document use_thys [
- "../../NumberTheory/Factorization",
- "BigO",
- "NatPair"
-];
-
-use_thys [
- "BinEx",
- "Sqrt",
- "Sqrt_Script",
- "NSPrimes",
- "BigO_Complex",
-
- "Arithmetic_Series_Complex",
- "HarmonicSeries",
-
- "DenumRat",
-
- "MIR",
- "ReflectedFerrack"
-];
-
--- a/src/HOL/Complex/ex/document/root.tex Tue Jul 01 07:13:45 2008 +0200
+++ b/src/HOL/Complex/ex/document/root.tex Tue Jul 01 07:58:17 2008 +0200
@@ -1,20 +0,0 @@
-
-\documentclass[11pt,a4paper]{article}
-\usepackage[latin1]{inputenc}
-\usepackage{isabelle,isabellesym}
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-
-\begin{document}
-
-\title{Miscellaneous HOL-Complex Examples}
-\maketitle
-
-\tableofcontents
-
-\parindent 0pt\parskip 0.5ex
-\input{session}
-
-\end{document}
--- a/src/HOL/IsaMakefile Tue Jul 01 07:13:45 2008 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 01 07:58:17 2008 +0200
@@ -5,9 +5,8 @@
## targets
default: HOL
-generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
-images: HOL-Plain HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
- HOL-Word TLA HOL4
+generate: HOL-Generate-HOL HOL-Generate-HOLLight
+images: HOL-Plain HOL HOL-Algebra HOL-Nominal HOL-Word TLA HOL4
#Note: keep targets sorted (except for HOL-Library and HOL-ex)
test: \
@@ -16,12 +15,11 @@
HOL-Auth \
HOL-AxClasses \
HOL-Bali \
- HOL-Complex-HahnBanach \
- HOL-Complex-Import \
- HOL-Complex-ex \
HOL-Extraction \
+ HOL-HahnBanach \
HOL-Hoare \
HOL-HoareParallel \
+ HOL-Import \
HOL-IMP \
HOL-IMPP \
HOL-IOA \
@@ -179,97 +177,19 @@
$(OUT)/HOL: $(OUT)/HOL-Plain \
ROOT.ML \
+ Arith_Tools.thy \
ATP_Linkup.thy \
- Arith_Tools.thy \
+ Complex/CLim.thy \
+ Complex/Complex_Main.thy \
+ Complex/Complex.thy \
+ Complex/CStar.thy \
+ Complex/Fundamental_Theorem_Algebra.thy \
+ Complex/NSCA.thy \
+ Complex/NSComplex.thy \
+ Complex/ROOT.ML \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
- Int.thy \
- IntDiv.thy \
- List.thy \
- Main.thy \
- Map.thy \
- NatBin.thy \
- Presburger.thy \
- Recdef.thy \
- Relation_Power.thy \
- SetInterval.thy \
- Tools/Groebner_Basis/groebner.ML \
- Tools/Groebner_Basis/misc.ML \
- Tools/Groebner_Basis/normalizer.ML \
- Tools/Groebner_Basis/normalizer_data.ML \
- Tools/Qelim/cooper.ML \
- Tools/Qelim/cooper_data.ML \
- Tools/Qelim/generated_cooper.ML \
- Tools/Qelim/presburger.ML \
- Tools/Qelim/qelim.ML \
- Tools/TFL/casesplit.ML \
- Tools/TFL/dcterm.ML \
- Tools/TFL/post.ML \
- Tools/TFL/rules.ML \
- Tools/TFL/tfl.ML \
- Tools/TFL/thms.ML \
- Tools/TFL/thry.ML \
- Tools/TFL/usyntax.ML \
- Tools/TFL/utils.ML \
- Tools/meson.ML \
- Tools/metis_tools.ML \
- Tools/numeral.ML \
- Tools/numeral_syntax.ML \
- Tools/polyhash.ML \
- Tools/recdef_package.ML \
- Tools/res_atp.ML \
- Tools/res_atp_methods.ML \
- Tools/res_atp_provers.ML \
- Tools/res_axioms.ML \
- Tools/res_clause.ML \
- Tools/res_hol_clause.ML \
- Tools/res_reconstruct.ML \
- Tools/specification_package.ML \
- Tools/string_syntax.ML \
- Tools/watcher.ML \
- int_arith1.ML \
- int_factor_simprocs.ML \
- nat_simprocs.ML \
- $(SRC)/Provers/Arith/assoc_fold.ML \
- $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
- $(SRC)/Provers/Arith/cancel_numerals.ML \
- $(SRC)/Provers/Arith/combine_numerals.ML \
- $(SRC)/Provers/Arith/extract_common_term.ML \
- $(SRC)/Tools/Metis/metis.ML
- @$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL-Plain HOL
-
-
-## HOL-Complex-HahnBanach
-
-HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
-
-$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex \
- Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
- Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
- Real/HahnBanach/HahnBanachExtLemmas.thy \
- Real/HahnBanach/HahnBanachSupLemmas.thy \
- Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
- Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
- Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
- Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
- Real/HahnBanach/document/root.tex
- @cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
-
-
-## HOL-Complex
-
-HOL-Complex: HOL $(OUT)/HOL-Complex
-
-$(OUT)/HOL-Complex: $(OUT)/HOL \
- Complex/ROOT.ML \
- Complex/CLim.thy \
- Complex/CStar.thy \
- Complex/Complex.thy \
- Complex/Complex_Main.thy \
- Complex/Fundamental_Theorem_Algebra.thy \
- Complex/NSCA.thy \
- Complex/NSComplex.thy \
Hyperreal/Deriv.thy \
Hyperreal/Fact.thy \
Hyperreal/Filter.thy \
@@ -282,22 +202,26 @@
Hyperreal/HyperDef.thy \
Hyperreal/HyperNat.thy \
Hyperreal/Hyperreal.thy \
+ Hyperreal/hypreal_arith.ML \
Hyperreal/Integration.thy \
Hyperreal/Lim.thy \
Hyperreal/Ln.thy \
Hyperreal/Log.thy \
Hyperreal/MacLaurin.thy \
+ Hyperreal/NatStar.thy \
Hyperreal/NSA.thy \
- Hyperreal/NatStar.thy \
Hyperreal/NthRoot.thy \
Hyperreal/SEQ.thy \
Hyperreal/Series.thy \
+ Hyperreal/StarDef.thy \
Hyperreal/Star.thy \
- Hyperreal/StarDef.thy \
Hyperreal/Taylor.thy \
Hyperreal/Transcendental.thy \
- Hyperreal/hypreal_arith.ML \
Hyperreal/transfer.ML \
+ int_arith1.ML \
+ IntDiv.thy \
+ int_factor_simprocs.ML \
+ Int.thy \
Library/Abstract_Rat.thy \
Library/Dense_Linear_Order.thy \
Library/GCD.thy \
@@ -306,36 +230,71 @@
Library/Parity.thy \
Library/Univ_Poly.thy \
Library/Zorn.thy \
+ List.thy \
+ Main.thy \
+ Map.thy \
+ NatBin.thy \
+ nat_simprocs.ML \
+ Presburger.thy \
Real/ContNotDenum.thy \
Real/Lubs.thy \
Real/PReal.thy \
- Real/RComplete.thy \
+ Real/rat_arith.ML \
Real/Rational.thy \
- Real/Real.thy \
+ Real/RComplete.thy \
+ Real/real_arith.ML \
Real/RealDef.thy \
Real/RealPow.thy \
+ Real/Real.thy \
Real/RealVector.thy \
- Real/rat_arith.ML \
- Real/real_arith.ML \
+ Recdef.thy \
+ Relation_Power.thy \
+ SetInterval.thy \
+ $(SRC)/Provers/Arith/assoc_fold.ML \
+ $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
+ $(SRC)/Provers/Arith/cancel_numerals.ML \
+ $(SRC)/Provers/Arith/combine_numerals.ML \
+ $(SRC)/Provers/Arith/extract_common_term.ML \
+ $(SRC)/Tools/Metis/metis.ML \
+ Tools/Groebner_Basis/groebner.ML \
+ Tools/Groebner_Basis/misc.ML \
+ Tools/Groebner_Basis/normalizer_data.ML \
+ Tools/Groebner_Basis/normalizer.ML \
+ Tools/meson.ML \
+ Tools/metis_tools.ML \
+ Tools/numeral.ML \
+ Tools/numeral_syntax.ML \
+ Tools/polyhash.ML \
+ Tools/Qelim/cooper_data.ML \
+ Tools/Qelim/cooper.ML \
+ Tools/Qelim/ferrante_rackoff_data.ML \
Tools/Qelim/ferrante_rackoff.ML \
- Tools/Qelim/ferrante_rackoff_data.ML \
+ Tools/Qelim/generated_cooper.ML \
+ Tools/Qelim/langford_data.ML \
Tools/Qelim/langford.ML \
- Tools/Qelim/langford_data.ML
- @cd Complex; $(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL HOL-Complex
-
-
-## HOL-Complex-ex
-
-HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
-
-$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
- Complex/ex/ROOT.ML Complex/ex/document/root.tex \
- Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
- Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy \
- Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML \
- Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy \
- Complex/ex/linreif.ML Complex/ex/linrtac.ML
- @cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
+ Tools/Qelim/presburger.ML \
+ Tools/Qelim/qelim.ML \
+ Tools/recdef_package.ML \
+ Tools/res_atp_methods.ML \
+ Tools/res_atp.ML \
+ Tools/res_atp_provers.ML \
+ Tools/res_axioms.ML \
+ Tools/res_clause.ML \
+ Tools/res_hol_clause.ML \
+ Tools/res_reconstruct.ML \
+ Tools/specification_package.ML \
+ Tools/string_syntax.ML \
+ Tools/TFL/casesplit.ML \
+ Tools/TFL/dcterm.ML \
+ Tools/TFL/post.ML \
+ Tools/TFL/rules.ML \
+ Tools/TFL/tfl.ML \
+ Tools/TFL/thms.ML \
+ Tools/TFL/thry.ML \
+ Tools/TFL/usyntax.ML \
+ Tools/TFL/utils.ML \
+ Tools/watcher.ML
+ @$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL-Plain HOL
## HOL-Library
@@ -371,6 +330,23 @@
@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
+## HOL-HahnBanach
+
+HOL-HahnBanach: HOL $(LOG)/HOL-HahnBanach.gz
+
+$(LOG)/HOL-HahnBanach.gz: $(OUT)/HOL \
+ Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
+ Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
+ Real/HahnBanach/HahnBanachExtLemmas.thy \
+ Real/HahnBanach/HahnBanachSupLemmas.thy \
+ Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
+ Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
+ Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
+ Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
+ Real/HahnBanach/document/root.tex
+ @cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL HahnBanach
+
+
## HOL-Subst
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
@@ -413,7 +389,7 @@
@$(ISATOOL) usedir $(OUT)/HOL IMPP
-## HOL-Complex-Import
+## HOL-Import
IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
@@ -425,38 +401,38 @@
Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
-HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz
+HOL-Import: HOL $(LOG)/HOL-Import.gz
-$(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)
- @$(ISATOOL) usedir $(OUT)/HOL-Complex Import
+$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
+ @$(ISATOOL) usedir $(OUT)/HOL Import
-## HOL-Complex-Generate-HOL
+## HOL-Generate-HOL
-HOL-Complex-Generate-HOL: HOL-Complex $(LOG)/HOL-Complex-Generate-HOL.gz
+HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz
-$(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex \
+$(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL \
$(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy \
Import/Generate-HOL/GenHOL4Prob.thy \
Import/Generate-HOL/GenHOL4Real.thy \
Import/Generate-HOL/GenHOL4Vec.thy \
Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
- @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL
+ @cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOL
-## HOL-Complex-Generate-HOLLight
+## HOL-Generate-HOLLight
-HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz
+HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
-$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex \
+$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \
$(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \
Import/Generate-HOLLight/ROOT.ML
- @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight
+ @cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOLLight
## HOL-Import-HOL
-HOL4: HOL-Complex $(LOG)/HOL4.gz
+HOL4: HOL $(LOG)/HOL4.gz
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
@@ -469,19 +445,19 @@
seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
word_base.imp word_bitop.imp word_num.imp
-$(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
+$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \
$(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \
Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \
Import/HOL/ROOT.ML
- @cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4
+ @cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL HOL4
-HOLLight: HOL-Complex $(LOG)/HOLLight.gz
+HOLLight: HOL $(LOG)/HOLLight.gz
-$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \
+$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \
Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
Import/HOLLight/ROOT.ML
- @cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOLLight
+ @cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL HOLLight
## HOL-NumberTheory
@@ -790,6 +766,7 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
+ Library/Primes.thy \
ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy \
ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy \
@@ -810,7 +787,12 @@
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy \
- ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
+ ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy \
+ Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
+ Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy \
+ Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML \
+ Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy \
+ Complex/ex/linreif.ML Complex/ex/linrtac.ML
@$(ISATOOL) usedir $(OUT)/HOL ex
@@ -844,11 +826,11 @@
@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
-## HOL-Complex-Matrix
+## HOL-Matrix
-HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
+HOL-Matrix: HOL $(OUT)/HOL-Matrix
-$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
+$(OUT)/HOL-Matrix: $(OUT)/HOL \
$(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
$(SRC)/Tools/Compute_Oracle/am_compiler.ML \
$(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
@@ -863,7 +845,7 @@
Matrix/cplex/FloatSparseMatrix.thy \
Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML
- @cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
+ @$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
## TLA
@@ -986,7 +968,7 @@
## clean
clean:
- @rm -f $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
+ @rm -f $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
$(LOG)/HOL.gz $(LOG)/TLA.gz \
$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
@@ -999,9 +981,7 @@
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
$(LOG)/HOL-Nominal-Examples.gz \
$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
- $(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
- $(LOG)/HOL-Complex.gz \
- $(LOG)/HOL-Complex-ex.gz \
- $(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
+ $(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
+ $(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz
--- a/src/HOL/ROOT.ML Tue Jul 01 07:13:45 2008 +0200
+++ b/src/HOL/ROOT.ML Tue Jul 01 07:58:17 2008 +0200
@@ -4,4 +4,4 @@
Classical Higher-order Logic -- batteries included.
*)
-use_thy "Main";
+use_thy "Complex/Complex_Main";
--- a/src/HOL/ex/ExecutableContent.thy Tue Jul 01 07:13:45 2008 +0200
+++ b/src/HOL/ex/ExecutableContent.thy Tue Jul 01 07:58:17 2008 +0200
@@ -6,17 +6,12 @@
theory ExecutableContent
imports
- Main
- Eval
- Enum
- Code_Index
- "~~/src/HOL/ex/Records"
+ Complex_Main
AssocList
Binomial
Commutative_Ring
- "~~/src/HOL/ex/Commutative_Ring_Complete"
- "~~/src/HOL/Real/RealDef"
- GCD
+ Enum
+ Eval
List_Prefix
Nat_Infinity
NatPair
@@ -29,11 +24,73 @@
State_Monad
While_Combinator
Word
+ "~~/src/HOL/ex/Commutative_Ring_Complete"
+ "~~/src/HOL/ex/Records"
begin
lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
declare fast_bv_to_nat_helper.simps [code func del]
+(*FIXME distribute to theories*)
+declare divides_def [code func del] -- "Univ_Poly"
+declare unstar_def [code func del] -- "StarDef"
+declare star_one_def [code func del] -- "StarDef"
+declare star_mult_def [code func del] -- "StarDef"
+declare star_add_def [code func del] -- "StarDef"
+declare star_zero_def [code func del] -- "StarDef"
+declare star_minus_def [code func del] -- "StarDef"
+declare star_diff_def [code func del] -- "StarDef"
+declare Reals_def [code func del] -- "RealVector"
+declare star_scaleR_def [code func del] -- "HyperDef"
+declare hyperpow_def [code func del] -- HyperDef
+declare Infinitesimal_def [code func del] -- NSA
+declare HFinite_def [code func del] -- NSA
+declare floor_def [code func del] -- RComplete
+declare LIMSEQ_def [code func del] -- SEQ
+declare partition_def [code func del] -- Integration
+declare Integral_def [code func del] -- Integration
+declare tpart_def [code func del] -- Integration
+declare psize_def [code func del] -- Integration
+declare gauge_def [code func del] -- Integration
+declare fine_def [code func del] -- Integration
+declare sumhr_def [code func del] -- HSeries
+declare NSsummable_def [code func del] -- HSeries
+declare NSLIMSEQ_def [code func del] -- HSEQ
+declare newInt.simps [code func del] -- ContNotDenum
+declare LIM_def [code func del] -- Lim
+declare NSLIM_def [code func del] -- HLim
+declare HComplex_def [code func del]
+declare of_hypnat_def [code func del]
+declare InternalSets_def [code func del]
+declare InternalFuns_def [code func del]
+declare increment_def [code func del]
+declare is_starext_def [code func del]
+declare hrcis_def [code func del]
+declare hexpi_def [code func del]
+declare hsgn_def [code func del]
+declare hcnj_def [code func del]
+declare hcis_def [code func del]
+declare harg_def [code func del]
+declare isNSUCont_def [code func del]
+declare hRe_def [code func del]
+declare hIm_def [code func del]
+declare HInfinite_def [code func del]
+declare hSuc_def [code func del]
+declare NSCauchy_def [code func del]
+declare of_hypreal_def [code func del]
+declare isNSCont_def [code func del]
+declare monoseq_def [code func del]
+declare scaleHR_def [code func del]
+declare isUCont_def [code func del]
+declare NSBseq_def [code func del]
+declare subseq_def [code func del]
+declare Cauchy_def [code func del]
+declare powhr_def [code func del]
+declare hlog_def [code func del]
+declare Zseq_def [code func del]
+declare Bseq_def [code func del]
+declare stc_def [code func del]
+
setup {*
Code.del_funcs
(AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))
--- a/src/HOL/ex/ROOT.ML Tue Jul 01 07:13:45 2008 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Jul 01 07:58:17 2008 +0200
@@ -87,3 +87,25 @@
HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
+no_document use_thys [
+ "../NumberTheory/Factorization",
+ "../Library/BigO",
+ "../Library/NatPair"
+];
+
+use_thys [
+ "../Complex/ex/BinEx",
+ "../Complex/ex/Sqrt",
+ "../Complex/ex/Sqrt_Script",
+ "../Complex/ex/NSPrimes",
+ "../Complex/ex/BigO_Complex",
+
+ "../Complex/ex/Arithmetic_Series_Complex",
+ "../Complex/ex/HarmonicSeries",
+
+ "../Complex/ex/DenumRat",
+
+ "../Complex/ex/MIR",
+ "../Complex/ex/ReflectedFerrack"
+];
+