| #
ee8e8234 |
|
06-Oct-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
a8dfe60c |
|
09-May-2014 |
haftmann <none@none> |
hardcoded nbe and sml into value command
|
| #
4c4ab66e |
|
19-Oct-2011 |
bulwahn <none@none> |
removing invocations of the evaluation method based on the old code generator
|
| #
e86659ab |
|
03-Aug-2011 |
bulwahn <none@none> |
removing value invocations with the SML code generator
|
| #
e4589447 |
|
27-Nov-2010 |
haftmann <none@none> |
tuned
|
| #
843cd228 |
|
26-Nov-2010 |
haftmann <none@none> |
tuned example
|
| #
b1671407 |
|
14-Jul-2009 |
haftmann <none@none> |
more canonical import
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
e9407033 |
|
20-Feb-2009 |
haftmann <none@none> |
stripped Id
|
| #
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
|
| #
cbeb4785 |
|
16-Sep-2008 |
haftmann <none@none> |
generic value command
|
| #
4c04d9ae |
|
31-Jan-2008 |
haftmann <none@none> |
proper term_of functions
|
| #
3b735b3d |
|
19-Oct-2007 |
haftmann <none@none> |
lemmas with normalization
|
| #
f242af43 |
|
08-Oct-2007 |
haftmann <none@none> |
simplified evaluation
|
| #
614afb50 |
|
04-Oct-2007 |
haftmann <none@none> |
clarified relationship of code generator conversions and evaluations
|
| #
d28159ce |
|
20-Sep-2007 |
haftmann <none@none> |
more permissive
|
| #
16b109b3 |
|
15-Sep-2007 |
haftmann <none@none> |
multi-functional value keyword
|
| #
e335e6ec |
|
24-Aug-2007 |
haftmann <none@none> |
overloaded definitions accompanied by explicit constants
|
| #
eaa48e3a |
|
16-Aug-2007 |
haftmann <none@none> |
added evaluation examples
|
| #
29547bde |
|
15-Aug-2007 |
haftmann <none@none> |
updated code generator setup
|
| #
1ebb9bfd |
|
05-Jun-2007 |
wenzelm <none@none> |
renamed ex/Eval_Examples.thy;
|