| #
0d89b02d |
|
31-Jul-2016 |
wenzelm <none@none> |
clarified imports;
|
| #
80cec798 |
|
31-Jul-2016 |
wenzelm <none@none> |
simplified theory structure;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
e9dd484d |
|
25-Mar-2013 |
hoelzl <none@none> |
move Ln.thy and Log.thy to Transcendental.thy
|
| #
e41352e0 |
|
25-Mar-2013 |
hoelzl <none@none> |
remove Real.thy
|
| #
7d344ad2 |
|
25-Mar-2013 |
hoelzl <none@none> |
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
--HG--
rename : src/HOL/SupInf.thy => src/HOL/Conditional_Complete_Lattices.thy
|
| #
36233165 |
|
01-Dec-2010 |
nipkow <none@none> |
moved activation of coercion inference into RealDef and declared function real a coercion.
Made use of it in theory Ln.
|
| #
6f80896a |
|
01-Dec-2010 |
wenzelm <none@none> |
activate subtyping/coercions in theory Complex_Main;
|
| #
ab51b555 |
|
22-Feb-2010 |
hoelzl <none@none> |
Replaced Integration by Multivariate-Analysis/Real_Integration
--HG--
rename : src/HOL/Multivariate_Analysis/Integration_MV.cert => src/HOL/Multivariate_Analysis/Integration.cert
rename : src/HOL/Multivariate_Analysis/Integration_MV.thy => src/HOL/Multivariate_Analysis/Integration.thy
|
| #
9f5057b6 |
|
26-Oct-2009 |
paulson <none@none> |
New theory SupInf of the supremum and infimum operators for sets of reals.
|
| #
5bf4488c |
|
19-May-2009 |
haftmann <none@none> |
moved Code_Index, Random and Quickcheck before Main
|
| #
011c72db |
|
16-May-2009 |
haftmann <none@none> |
experimental move of Quickcheck and related theories to HOL image
--HG--
rename : src/HOL/Library/Code_Index.thy => src/HOL/Code_Index.thy
rename : src/HOL/Library/Quickcheck.thy => src/HOL/Quickcheck.thy
rename : src/HOL/Library/Random.thy => src/HOL/Random.thy
|
| #
e73d2d8e |
|
15-May-2009 |
haftmann <none@none> |
experimental addition of quickcheck
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
9dbac01a |
|
18-Feb-2009 |
huffman <none@none> |
move FrechetDeriv.thy to Library
--HG--
rename : src/HOL/FrechetDeriv.thy => src/HOL/Library/FrechetDeriv.thy
|
| #
db02b24a |
|
12-Feb-2009 |
nipkow <none@none> |
Moved FTA into Lib and cleaned it up a little.
--HG--
rename : src/HOL/Fundamental_Theorem_Algebra.thy => src/HOL/Library/Fundamental_Theorem_Algebra.thy
|
| #
1205bcd3 |
|
01-Jan-2009 |
wenzelm <none@none> |
tuned header and description of boot files;
|
| #
66194568 |
|
29-Dec-2008 |
haftmann <none@none> |
adapted HOL source structure to distribution layout
--HG--
rename : src/HOL/Library/Dense_Linear_Order.thy => src/HOL/Dense_Linear_Order.thy
rename : src/HOL/Complex/Fundamental_Theorem_Algebra.thy => src/HOL/Fundamental_Theorem_Algebra.thy
rename : src/HOL/Real/HahnBanach/Bounds.thy => src/HOL/HahnBanach/Bounds.thy
rename : src/HOL/Real/HahnBanach/FunctionNorm.thy => src/HOL/HahnBanach/FunctionNorm.thy
rename : src/HOL/Real/HahnBanach/FunctionOrder.thy => src/HOL/HahnBanach/FunctionOrder.thy
rename : src/HOL/Real/HahnBanach/HahnBanach.thy => src/HOL/HahnBanach/HahnBanach.thy
rename : src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy => src/HOL/HahnBanach/HahnBanachExtLemmas.thy
rename : src/HOL/Real/HahnBanach/HahnBanachLemmas.thy => src/HOL/HahnBanach/HahnBanachLemmas.thy
rename : src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy => src/HOL/HahnBanach/HahnBanachSupLemmas.thy
rename : src/HOL/Real/HahnBanach/Linearform.thy => src/HOL/HahnBanach/Linearform.thy
rename : src/HOL/Real/HahnBanach/NormedSpace.thy => src/HOL/HahnBanach/NormedSpace.thy
rename : src/HOL/Real/HahnBanach/README.html => src/HOL/HahnBanach/README.html
rename : src/HOL/Real/HahnBanach/ROOT.ML => src/HOL/HahnBanach/ROOT.ML
rename : src/HOL/Real/HahnBanach/Subspace.thy => src/HOL/HahnBanach/Subspace.thy
rename : src/HOL/Real/HahnBanach/VectorSpace.thy => src/HOL/HahnBanach/VectorSpace.thy
rename : src/HOL/Real/HahnBanach/ZornLemma.thy => src/HOL/HahnBanach/ZornLemma.thy
rename : src/HOL/Real/HahnBanach/document/root.bib => src/HOL/HahnBanach/document/root.bib
rename : src/HOL/Real/HahnBanach/document/root.tex => src/HOL/HahnBanach/document/root.tex
rename : src/HOL/Real/RealVector.thy => src/HOL/RealVector.thy
rename : src/HOL/Hyperreal/SEQ.thy => src/HOL/SEQ.thy
|
| #
7fe13fce |
|
10-Dec-2008 |
nipkow <none@none> |
moved ContNotDenum into Library
--HG--
rename : src/HOL/ContNotDenum.thy => src/HOL/Library/ContNotDenum.thy
|
| #
f21befe1 |
|
03-Dec-2008 |
haftmann <none@none> |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML
|