| #
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
4125d2fe |
|
28-Jul-2015 |
wenzelm <none@none> |
more explicit context;
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
c97e9ad6 |
|
07-Mar-2015 |
wenzelm <none@none> |
clarified Drule.gen_all: observe context more carefully;
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
2257dcda |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
8aa502e5 |
|
12-Jan-2014 |
wenzelm <none@none> |
tuned signature;
clarified context;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
| #
ed870e69 |
|
15-Mar-2012 |
paulson <none@none> |
replacing ":" by "\<in>"
|
| #
f557cea7 |
|
08-Mar-2012 |
paulson <none@none> |
Structured and calculation-based proofs (with new trans rules!)
|
| #
8125fbfb |
|
06-Mar-2012 |
paulson <none@none> |
Using mathematical notation for <-> and cardinal arithmetic
|
| #
f902d62a |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols instead of ASCII
|
| #
1d553e50 |
|
24-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
| #
7bae4824 |
|
23-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
| #
29168e90 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
14ffc3e9 |
|
13-May-2011 |
wenzelm <none@none> |
clarified map_simpset versus Simplifier.map_simpset_global;
|
| #
335dc010 |
|
13-May-2011 |
wenzelm <none@none> |
make ZF_cs snapshot after final setup;
|
| #
c6e0bbb6 |
|
22-Apr-2011 |
wenzelm <none@none> |
misc tuning and simplification;
|
| #
b95224b1 |
|
22-Apr-2011 |
wenzelm <none@none> |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;
|
| #
f1968c93 |
|
22-Apr-2011 |
wenzelm <none@none> |
modernized Quantifier1 simproc setup;
|
| #
612170a9 |
|
18-Feb-2011 |
wenzelm <none@none> |
more precise headers;
|
| #
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
|
| #
e7a16ceb |
|
07-Oct-2007 |
wenzelm <none@none> |
modernized specifications;
removed legacy ML bindings;
|
| #
82fde663 |
|
02-Aug-2005 |
wenzelm <none@none> |
tuned;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
40cb56a5 |
|
02-Jun-2004 |
paulson <none@none> |
new rules for simplifying quantifiers with Sigma
|
| #
287028e5 |
|
28-Aug-2002 |
paulson <none@none> |
various new lemmas for Constructible
|
| #
43f1782a |
|
14-Jul-2002 |
paulson <none@none> |
Removal of mono.thy
|
| #
35c9abf2 |
|
23-Jun-2002 |
paulson <none@none> |
conversion of Sum, pair to Isar script
|
| #
1848838c |
|
05-Oct-2001 |
wenzelm <none@none> |
tuned;
|
| #
8e86760f |
|
10-Aug-2000 |
paulson <none@none> |
installation of cancellation simprocs for the integers
|
| #
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
| #
5c777ea1 |
|
16-Nov-1993 |
clasohm <none@none> |
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
|