| #
eb030641 |
|
02-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
| #
ee8e8234 |
|
06-Oct-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
763a4215 |
|
01-Apr-2015 |
paulson <lp15@cam.ac.uk> |
John Harrison's example: a 32-bit approximation to pi. SLOW
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
6a02610c |
|
21-Sep-2014 |
haftmann <none@none> |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
| #
9a54c133 |
|
22-Nov-2011 |
huffman <none@none> |
remove outdated comment
|
| #
458f79cc |
|
08-May-2009 |
haftmann <none@none> |
explicit method linarith
|
| #
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
|
| #
a33601ad |
|
01-Oct-2006 |
wenzelm <none@none> |
tuned;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
f2340401 |
|
16-May-2005 |
paulson <none@none> |
Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ
|
| #
950528a4 |
|
30-Jun-2004 |
paulson <none@none> |
new treatment of binary numerals
|
| #
29c20de7 |
|
19-Feb-2004 |
ballarin <none@none> |
Efficient, graph-based reasoner for linear and partial orders.
+ Setup as solver in the HOL simplifier.
|
| #
4cb77476 |
|
09-Feb-2004 |
paulson <none@none> |
generic of_nat and of_int functions, and generalization of iszero
and neg
|
| #
ef14d5f4 |
|
22-Jul-2003 |
paulson <none@none> |
Added some regression testing for simprocs
|
| #
8a9f3c8f |
|
15-Jul-2003 |
paulson <none@none> |
Fixing a simproc bug
|
| #
f9f7966a |
|
12-Aug-2002 |
nipkow <none@none> |
*** empty log message ***
|
| #
9a12fac4 |
|
30-May-2002 |
paulson <none@none> |
fixed a proof near the end
|
| #
3690eeb2 |
|
30-May-2002 |
nipkow <none@none> |
Modifications due to enhanced linear arithmetic.
|
| #
ca26b699 |
|
02-Jan-2002 |
paulson <none@none> |
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
|
| #
fb4bd978 |
|
22-Oct-2001 |
paulson <none@none> |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
to their abstract counterparts, while other binary numerals work correctly.
|
| #
f96783a0 |
|
05-Oct-2001 |
wenzelm <none@none> |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
| #
6ddaa347 |
|
05-Oct-2001 |
wenzelm <none@none> |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
|
| #
bb4f8581 |
|
28-Sep-2001 |
wenzelm <none@none> |
inductive: no collective atts;
|
| #
256c6a6f |
|
01-Feb-2001 |
wenzelm <none@none> |
converted to new-style theories;
|
| #
342cf7c2 |
|
13-Jul-2000 |
wenzelm <none@none> |
tuned;
|
| #
961b49b4 |
|
08-Jul-1999 |
paulson <none@none> |
Introduction of integer division algorithm
|
| #
7809d59c |
|
24-Sep-1998 |
paulson <none@none> |
added correctness proofs for arithmetic
|
| #
bf71379d |
|
24-Jul-1998 |
wenzelm <none@none> |
added ex/MonoidGroups (record example);
moved Bin and String examples to ex;
|