2021-09-19 |
wenzelm |
clarified signature -- prefer antiquotations (with subtle change of exception content);
|
file |
diff |
annotate
|
2021-09-11 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
2020-05-30 |
haftmann |
specific atomization inert to later rule set modifications
|
file |
diff |
annotate
|
2019-01-04 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
2016-08-09 |
nipkow |
adapted ZF,FOL,CCL,LCF to modified splitter
|
file |
diff |
annotate
|
2015-07-28 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
2015-04-08 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
2015-03-07 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
2015-03-04 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
2015-02-10 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
2014-11-10 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
2014-11-09 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
2014-10-30 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
2014-03-21 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
2014-01-12 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
2011-11-28 |
wenzelm |
avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
|
file |
diff |
annotate
|
2011-11-24 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
2011-11-23 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
2011-06-29 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
2011-06-29 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
2011-05-13 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
2011-04-26 |
wenzelm |
modernized Clasimp setup;
|
file |
diff |
annotate
|
2011-04-22 |
wenzelm |
simplified Data signature;
|
file |
diff |
annotate
|
2011-04-22 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
2011-04-22 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
2011-04-22 |
wenzelm |
clarified simpset setup;
|
file |
diff |
annotate
|
2010-12-20 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
2010-08-25 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
2010-08-17 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
2010-04-30 |
wenzelm |
removed some old comments;
|
file |
diff |
annotate
|
2010-04-30 |
wenzelm |
proper context for rule_by_tactic;
|
file |
diff |
annotate
|
2010-04-29 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
2010-02-19 |
wenzelm |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
2010-02-07 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
2009-10-16 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
2009-10-15 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
2009-07-24 |
wenzelm |
renamed functor SplitterFun to Splitter, require explicit theory;
|
file |
diff |
annotate
|
2009-07-23 |
wenzelm |
more @{theory} antiquotations;
|
file |
diff |
annotate
|
2009-07-23 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
2009-07-15 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
2009-07-09 |
wenzelm |
removed obsolete CVS Ids;
|
file |
diff |
annotate
|
2009-03-20 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file |
diff |
annotate
|
2008-09-17 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
2008-06-24 |
wenzelm |
ML_Antiquote.value;
|
file |
diff |
annotate
|
2008-03-29 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
2008-03-15 |
wenzelm |
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
|
file |
diff |
annotate
|
2007-04-27 |
wenzelm |
removed obsolete induct/simp tactic;
|
file |
diff |
annotate
|
2007-01-20 |
wenzelm |
added @{clasimpset};
|
file |
diff |
annotate
|
2006-11-26 |
wenzelm |
converted legacy ML scripts;
|
file |
diff |
annotate
|
2006-07-27 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2006-01-19 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
2005-12-31 |
wenzelm |
removed obsolete Provers/make_elim.ML;
|
file |
diff |
annotate
|
2005-12-01 |
wenzelm |
unfold_tac: static evaluation of simpset;
|
file |
diff |
annotate
|
2005-10-18 |
wenzelm |
Simplifier.theory_context;
|
file |
diff |
annotate
|
2005-10-17 |
wenzelm |
change_claset/simpset;
|
file |
diff |
annotate
|
2005-09-12 |
haftmann |
introduced new-style AList operations
|
file |
diff |
annotate
|
2005-08-02 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
2005-05-22 |
wenzelm |
Simplifier already setup in Pure;
|
file |
diff |
annotate
|
2005-03-03 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|