| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
| #
950a6e9d |
|
01-Jan-2018 |
haftmann <none@none> |
tuned
--HG--
extra : rebase_source : abc778c1dd7d6e28bb98ffb72dddfb42c0c64085
|
| #
0e1ddc68 |
|
09-Aug-2016 |
nipkow <none@none> |
introduced aggressive splitter "split!"
|
| #
4125d2fe |
|
28-Jul-2015 |
wenzelm <none@none> |
more explicit context;
|
| #
6fd8f006 |
|
05-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
| #
84c9c105 |
|
04-May-2015 |
nipkow <none@none> |
no more simp_legacy_precond
|
| #
cff2e75b |
|
08-Apr-2015 |
wenzelm <none@none> |
proper context for Object_Logic operations;
|
| #
c97e9ad6 |
|
07-Mar-2015 |
wenzelm <none@none> |
clarified Drule.gen_all: observe context more carefully;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
a9c547a6 |
|
10-Feb-2015 |
wenzelm <none@none> |
misc tuning;
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
047449b8 |
|
21-Dec-2014 |
wenzelm <none@none> |
proper context;
|
| #
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
| #
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
| #
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
| #
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
713cd402 |
|
13-Mar-2014 |
nipkow <none@none> |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
--HG--
extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893
|
| #
8aa502e5 |
|
12-Jan-2014 |
wenzelm <none@none> |
tuned signature;
clarified context;
|
| #
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
1d553e50 |
|
24-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
| #
01933827 |
|
23-Nov-2011 |
wenzelm <none@none> |
tuned;
|
| #
7bae4824 |
|
23-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
| #
a9de3adb |
|
29-Jun-2011 |
wenzelm <none@none> |
tuned signature;
|
| #
9c72c6e0 |
|
29-Jun-2011 |
wenzelm <none@none> |
simplified/unified Simplifier.mk_solver;
|
| #
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
| #
5585cb3d |
|
26-Apr-2011 |
wenzelm <none@none> |
modernized Clasimp setup;
|
| #
7f6fd60f |
|
22-Apr-2011 |
wenzelm <none@none> |
simplified Data signature;
|
| #
ebf09630 |
|
22-Apr-2011 |
wenzelm <none@none> |
misc tuning;
|
| #
f1968c93 |
|
22-Apr-2011 |
wenzelm <none@none> |
modernized Quantifier1 simproc setup;
|
| #
b4763bb2 |
|
21-Apr-2011 |
wenzelm <none@none> |
clarified simpset setup;
discontinued unused old-style FOL_css;
|
| #
d1a2ff7b |
|
16-Apr-2011 |
wenzelm <none@none> |
eliminated old List.nth;
tuned;
|
| #
b11705e1 |
|
28-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix equality now named HOL.eq
|
| #
c91cbd4e |
|
27-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
| #
5f258a36 |
|
26-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix impliciation now named HOL.implies
|
| #
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;
|
| #
33076e76 |
|
19-Aug-2010 |
haftmann <none@none> |
tuned quotes
|
| #
dd7c556c |
|
08-Jul-2010 |
haftmann <none@none> |
tuned titles
|
| #
9430482e |
|
30-Apr-2010 |
wenzelm <none@none> |
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
|
| #
b96c5111 |
|
29-Apr-2010 |
wenzelm <none@none> |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
| #
97f02687 |
|
25-Feb-2010 |
wenzelm <none@none> |
more antiquotations;
|
| #
aa047a26 |
|
19-Feb-2010 |
wenzelm <none@none> |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
| #
28238a3e |
|
29-Oct-2009 |
wenzelm <none@none> |
eliminated some old folds;
|
| #
4137057a |
|
24-Jul-2009 |
wenzelm <none@none> |
renamed functor SplitterFun to Splitter, require explicit theory;
|
| #
92e775bc |
|
23-Jul-2009 |
wenzelm <none@none> |
more @{theory} antiquotations;
|
| #
a4b600c4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
| #
a5a5665f |
|
15-Jul-2009 |
wenzelm <none@none> |
more antiquotations;
|
| #
1716138f |
|
20-Mar-2009 |
wenzelm <none@none> |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
d647eb14 |
|
01-Mar-2009 |
wenzelm <none@none> |
use long names for old-style fold combinators;
|
| #
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
|