| 2010-08-27 |
wenzelm |
2010-08-27 |
more careful treatment of context visibility flag wrt. spurious warnings;
misc tuning;
|
file | diff | annotate |
| 2010-08-25 |
wenzelm |
2010-08-25 |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2010-05-15 |
wenzelm |
2010-05-15 |
less pervasive names from structure Thm;
|
file | diff | annotate |
| 2010-05-03 |
wenzelm |
2010-05-03 |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2010-04-30 |
wenzelm |
2010-04-30 |
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
|
file | diff | annotate |
| 2010-04-29 |
wenzelm |
2010-04-29 |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file | diff | annotate |
| 2010-04-26 |
wenzelm |
2010-04-26 |
eliminanated some unreferenced identifiers;
tuned;
|
file | diff | annotate |
| 2010-03-29 |
boehmes |
2010-03-29 |
the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value
|
file | diff | annotate |
| 2010-03-28 |
wenzelm |
2010-03-28 |
static defaults for configuration options;
|
file | diff | annotate |
| 2010-03-27 |
boehmes |
2010-03-27 |
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
|
file | diff | annotate |
| 2010-03-26 |
boehmes |
2010-03-26 |
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
|
file | diff | annotate |
| 2010-03-20 |
wenzelm |
2010-03-20 |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file | diff | annotate |
| 2010-02-27 |
wenzelm |
2010-02-27 |
modernized structure Term_Ord;
|
file | diff | annotate |
| 2010-02-19 |
wenzelm |
2010-02-19 |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2010-02-19 |
wenzelm |
2010-02-19 |
tuned message;
|
file | diff | annotate |
| 2009-11-25 |
haftmann |
2009-11-25 |
normalized uncurry take/drop
|
file | diff | annotate |
| 2009-11-24 |
haftmann |
2009-11-24 |
curried take/drop
|
file | diff | annotate |
| 2009-11-08 |
wenzelm |
2009-11-08 |
tuned;
|
file | diff | annotate |
| 2009-11-02 |
wenzelm |
2009-11-02 |
back to warning -- Proof General tends to "popup" tracing output;
|
file | diff | annotate |
| 2009-10-29 |
wenzelm |
2009-10-29 |
less aggressive tracing;
|
file | diff | annotate |
| 2009-10-27 |
wenzelm |
2009-10-27 |
eliminated some old folds;
|
file | diff | annotate |
| 2009-10-21 |
haftmann |
2009-10-21 |
merged
|
file | diff | annotate |
| 2009-10-21 |
haftmann |
2009-10-21 |
dropped redundant gen_ prefix
|
file | diff | annotate |
| 2009-10-20 |
haftmann |
2009-10-20 |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file | diff | annotate |
| 2009-10-20 |
wenzelm |
2009-10-20 |
backpatching of structure Proof and ProofContext -- avoid odd aliases;
renamed transfer_proof to raw_transfer;
indicate firm naming conventions for theory, Proof.context, Context.generic;
|
file | diff | annotate |
| 2009-10-20 |
wenzelm |
2009-10-20 |
uniform use of Integer.min/max;
|
file | diff | annotate |
| 2009-09-30 |
wenzelm |
2009-09-30 |
eliminated dead code;
eliminated redundant bindings;
misc tuning;
|
file | diff | annotate |
| 2009-09-29 |
wenzelm |
2009-09-29 |
explicit indication of Unsynchronized.ref;
|
file | diff | annotate |
| 2009-05-30 |
wenzelm |
2009-05-30 |
tuned;
|
file | diff | annotate |
| 2009-04-21 |
krauss |
2009-04-21 |
replace type cong = {thm : thm, lhs : term} by plain thm -- the other component has been unused for a long time.
|
file | diff | annotate |
| 2009-03-16 |
wenzelm |
2009-03-16 |
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
|
file | diff | annotate |
| 2009-03-08 |
wenzelm |
2009-03-08 |
added dest_ss;
proper context fo pretty_ss;
tuned;
|
file | diff | annotate |
| 2009-03-07 |
wenzelm |
2009-03-07 |
renamed rep_ss to MetaSimplifier.internal_ss;
|
file | diff | annotate |
| 2009-03-06 |
wenzelm |
2009-03-06 |
replaced archaic use of rep_ss by Simplifier.mksimps;
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
|
file | diff | annotate |
| 2008-11-18 |
wenzelm |
2008-11-18 |
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
eliminated obsolete alias rewtac for rewrite_goals_tac;
|
file | diff | annotate |
| 2008-10-16 |
wenzelm |
2008-10-16 |
Drule.norm_hhf_eqs;
|
file | diff | annotate |
| 2008-08-14 |
wenzelm |
2008-08-14 |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file | diff | annotate |
| 2008-07-14 |
haftmann |
2008-07-14 |
dropped junk
|
file | diff | annotate |
| 2008-07-14 |
haftmann |
2008-07-14 |
added further simple interfaces
|
file | diff | annotate |
| 2008-06-21 |
wenzelm |
2008-06-21 |
activate_context: strict the_context, no fallback on theory context;
|
file | diff | annotate |
| 2008-05-29 |
wenzelm |
2008-05-29 |
legacy_feature: no proof context in simpset;
|
file | diff | annotate |
| 2008-05-18 |
wenzelm |
2008-05-18 |
moved global pretty/string_of functions from Sign to Syntax;
|
file | diff | annotate |
| 2008-04-12 |
wenzelm |
2008-04-12 |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file | diff | annotate |
| 2008-03-27 |
wenzelm |
2008-03-27 |
eliminated theory ProtoPure;
|
file | diff | annotate |
| 2007-11-27 |
berghofe |
2007-11-27 |
check_conv now only performs beta-eta-normalization when equations
cannot be combined just by transitivity.
|
file | diff | annotate |
| 2007-10-26 |
wenzelm |
2007-10-26 |
asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
|
file | diff | annotate |
| 2007-09-25 |
wenzelm |
2007-09-25 |
Syntax.parse/check/read;
|
file | diff | annotate |
| 2007-08-20 |
wenzelm |
2007-08-20 |
tuned merge operations via pointer_eq;
|
file | diff | annotate |
| 2007-08-02 |
wenzelm |
2007-08-02 |
turned simp_depth_limit into configuration option;
|
file | diff | annotate |
| 2007-07-23 |
wenzelm |
2007-07-23 |
depth flag: plain bool ref;
eliminated transform_failure (to avoid critical section for main transactions);
|
file | diff | annotate |
| 2007-07-05 |
wenzelm |
2007-07-05 |
tuned;
|
file | diff | annotate |
| 2007-07-05 |
wenzelm |
2007-07-05 |
tuned goal conversion interfaces;
|
file | diff | annotate |
| 2007-07-03 |
wenzelm |
2007-07-03 |
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
|
file | diff | annotate |
| 2007-06-03 |
wenzelm |
2007-06-03 |
merge_ss: plain merge of prems;
|
file | diff | annotate |
| 2007-05-31 |
wenzelm |
2007-05-31 |
simplified/unified list fold;
|
file | diff | annotate |
| 2007-05-10 |
wenzelm |
2007-05-10 |
moved some Drule operations to Thm (see more_thm.ML);
|
file | diff | annotate |
| 2007-05-09 |
wenzelm |
2007-05-09 |
simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification);
trace_simp_depth_limit_exceeded: attempt to hide destructive pointer programming within simpset;
|
file | diff | annotate |
| 2007-04-16 |
haftmann |
2007-04-16 |
canonical merge operations
|
file | diff | annotate |
| 2007-04-14 |
wenzelm |
2007-04-14 |
Morphism.transform/form;
|
file | diff | annotate |