| #
caa31cef |
|
22-Jun-2019 |
haftmann <none@none> |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
| #
f827427c |
|
02-Dec-2017 |
haftmann <none@none> |
cleaned up and tuned
--HG--
extra : rebase_source : a1262817f08e7c73c1f578e8c3b21fcf9314f1fb
|
| #
81b459a5 |
|
08-Apr-2016 |
wenzelm <none@none> |
eliminated unused simproc identifier;
|
| #
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
| #
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
34ef1352 |
|
10-Apr-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
7ac6d7e8 |
|
04-Nov-2013 |
haftmann <none@none> |
streamlined setup of linear arithmetic
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
dffabb9f |
|
30-Mar-2012 |
huffman <none@none> |
add constant pred_numeral k = numeral k - (1::nat);
replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral
|
| #
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
| #
8cd5b4bf |
|
29-Jun-2011 |
wenzelm <none@none> |
modernized some simproc setup;
|
| #
14ffc3e9 |
|
13-May-2011 |
wenzelm <none@none> |
clarified map_simpset versus Simplifier.map_simpset_global;
|
| #
b11705e1 |
|
28-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix equality now named HOL.eq
|
| #
2c483e55 |
|
26-Aug-2010 |
wenzelm <none@none> |
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
|
| #
2ab2e08e |
|
25-Aug-2010 |
wenzelm <none@none> |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
| #
dc514061 |
|
15-May-2010 |
wenzelm <none@none> |
less pervasive names from structure Thm;
|
| #
3aa9f578 |
|
19-Feb-2010 |
haftmann <none@none> |
moved remaning class operations from Algebras.thy to Groups.thy
|
| #
75f69d99 |
|
10-Feb-2010 |
haftmann <none@none> |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
| #
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
| #
7b3a0878 |
|
28-Jan-2010 |
haftmann <none@none> |
new theory Algebras.thy for generic algebraic structures
|
| #
0f96c7cc |
|
28-Oct-2009 |
haftmann <none@none> |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
| #
37b6b840 |
|
18-Sep-2009 |
haftmann <none@none> |
tuned const_name antiquotations
|
| #
9901e5e8 |
|
08-Jun-2009 |
boehmes <none@none> |
fast_lin_arith uses proper multiplication instead of unfolding to additions
|
| #
7bec761b |
|
11-May-2009 |
haftmann <none@none> |
qualified names for Lin_Arith tactics and simprocs
|
| #
180d846c |
|
11-May-2009 |
haftmann <none@none> |
tuned interface of Lin_Arith
|
| #
88ceafba |
|
09-May-2009 |
haftmann <none@none> |
interface changes in linarith.ML
|
| #
e7ae535a |
|
08-May-2009 |
haftmann <none@none> |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
--HG--
rename : src/HOL/Tools/nat_simprocs.ML => src/HOL/Tools/nat_numeral_simprocs.ML
rename : src/HOL/Tools/int_factor_simprocs.ML => src/HOL/Tools/numeral_simprocs.ML
|
| #
f24ced81 |
|
29-Apr-2009 |
huffman <none@none> |
reimplement reorientation simproc using theory data
|
| #
33ab498d |
|
30-Mar-2009 |
huffman <none@none> |
simplify theorem references
|
| #
5c4d5b37 |
|
26-Mar-2009 |
huffman <none@none> |
parameterize assoc_fold with is_numeral predicate
|
| #
ba09f385 |
|
23-Mar-2009 |
haftmann <none@none> |
structure LinArith now named Lin_Arith
|
| #
0296373a |
|
13-Mar-2009 |
haftmann <none@none> |
moved some generic nonsense to arith_data.ML
|
| #
4957cf6d |
|
12-Mar-2009 |
haftmann <none@none> |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
--HG--
rename : src/HOL/Tools/arith_data.ML => src/HOL/Tools/nat_arith.ML
|
| #
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
|
| #
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
|