| 2010-08-25 |
wenzelm |
2010-08-25 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| 2010-06-03 |
wenzelm |
2010-06-03 |
eliminated ML structure alias;
|
file | diff | annotate |
| 2010-06-02 |
wenzelm |
2010-06-02 |
always unconstrain thm proofs;
|
file | diff | annotate |
| 2010-05-19 |
haftmann |
2010-05-19 |
dropped legacy_unconstrainT
|
file | diff | annotate |
| 2010-05-14 |
wenzelm |
2010-05-14 |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
file | diff | annotate |
| 2010-05-13 |
wenzelm |
2010-05-13 |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
file | diff | annotate |
| 2010-05-09 |
wenzelm |
2010-05-09 |
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
|
file | diff | annotate |
| 2010-05-09 |
wenzelm |
2010-05-09 |
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
|
file | diff | annotate |
| 2010-05-09 |
wenzelm |
2010-05-09 |
just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;
|
file | diff | annotate |
| 2010-05-08 |
wenzelm |
2010-05-08 |
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
|
file | diff | annotate |
| 2010-05-08 |
wenzelm |
2010-05-08 |
tuned signature;
|
file | diff | annotate |
| 2010-05-04 |
wenzelm |
2010-05-04 |
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
* present type variables are only compared wrt. first component (the atomic type), not the duplicated sort;
* extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem);
* deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;
|
file | diff | annotate |
| 2010-05-04 |
wenzelm |
2010-05-04 |
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
|
file | diff | annotate |
| 2010-05-03 |
wenzelm |
2010-05-03 |
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
file | diff | annotate |
| 2010-05-03 |
wenzelm |
2010-05-03 |
minor tuning of Thm.strip_shyps -- no longer pervasive;
|
file | diff | annotate |
| 2010-05-03 |
wenzelm |
2010-05-03 |
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
|
file | diff | annotate |
| 2010-04-25 |
wenzelm |
2010-04-25 |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
less pervasive names;
|
file | diff | annotate |
| 2010-03-27 |
wenzelm |
2010-03-27 |
added Term.fold_atyps_sorts convenience;
|
file | diff | annotate |
| 2010-03-21 |
wenzelm |
2010-03-21 |
Logic.mk_of_sort convenience;
|
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 |
| 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-21 |
wenzelm |
2009-11-21 |
explicitly mark some legacy freeze operations;
|
file | diff | annotate |
| 2009-11-16 |
wenzelm |
2009-11-16 |
generalized procs for rewrite_proof: allow skeleton;
fulfill_norm_proof: always normalize result here, no re-normalization after filling;
|
file | diff | annotate |
| 2009-11-15 |
wenzelm |
2009-11-15 |
tuned;
|
file | diff | annotate |
| 2009-11-08 |
wenzelm |
2009-11-08 |
adapted Theory_Data;
tuned;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
make SML/NJ happy;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file | diff | annotate |
| 2009-10-21 |
haftmann |
2009-10-21 |
curried inter as canonical list operation (beware of argument order)
|
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-01 |
wenzelm |
2009-10-01 |
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
|
file | diff | annotate |
| 2009-09-30 |
wenzelm |
2009-09-30 |
eliminated redundant bindings;
|
file | diff | annotate |
| 2009-09-28 |
wenzelm |
2009-09-28 |
fold_body_thms: pass pthm identifier;
fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen";
fulfill_proof/thm_proof: check for thm cycles at the substitution point;
|
file | diff | annotate |
| 2009-09-28 |
wenzelm |
2009-09-28 |
tuned internal source structure;
|
file | diff | annotate |
| 2009-09-16 |
wenzelm |
2009-09-16 |
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
|
file | diff | annotate |
| 2009-07-26 |
wenzelm |
2009-07-26 |
lambda/cabs/all: named variants;
|
file | diff | annotate |
| 2009-07-21 |
wenzelm |
2009-07-21 |
simultaneous join_proofs;
removed obsolete promises_of;
|
file | diff | annotate |
| 2009-07-21 |
wenzelm |
2009-07-21 |
prefer simultaneous join -- for improved scheduling;
|
file | diff | annotate |
| 2009-07-19 |
wenzelm |
2009-07-19 |
support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
export promises_of;
removed obsolete pending_groups;
tuned;
|
file | diff | annotate |
| 2009-07-17 |
wenzelm |
2009-07-17 |
tuned/modernized Envir.subst_XXX;
|
file | diff | annotate |
| 2009-07-17 |
wenzelm |
2009-07-17 |
tuned/modernized Envir operations;
|
file | diff | annotate |
| 2009-07-16 |
wenzelm |
2009-07-16 |
tuned incr_indexes;
|
file | diff | annotate |
| 2009-07-09 |
wenzelm |
2009-07-09 |
renamed structure TermSubst to Term_Subst;
|
file | diff | annotate |
| 2009-07-06 |
wenzelm |
2009-07-06 |
clarified strip_shyps: proper type witnesses for present sorts;
moved fold_terms to thm.ML;
|
file | diff | annotate |
| 2009-07-06 |
wenzelm |
2009-07-06 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| 2009-07-06 |
wenzelm |
2009-07-06 |
clarified Thm.of_class/of_sort/class_triv;
|
file | diff | annotate |
| 2009-07-06 |
wenzelm |
2009-07-06 |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
file | diff | annotate |
| 2009-07-02 |
wenzelm |
2009-07-02 |
strip_shyps: remove top sort, which is logically insignificant;
|
file | diff | annotate |
| 2009-07-02 |
wenzelm |
2009-07-02 |
added pro-forma proof constructor Inclass;
|
file | diff | annotate |
| 2009-03-25 |
wenzelm |
2009-03-25 |
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
more explicit oracle_proof;
|
file | diff | annotate |
| 2009-03-24 |
wenzelm |
2009-03-24 |
status_of: need to include local promises as well!
|
file | diff | annotate |
| 2009-03-24 |
wenzelm |
2009-03-24 |
display derivation status of thms;
|
file | diff | annotate |
| 2009-03-17 |
wenzelm |
2009-03-17 |
eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
tuned;
|
file | diff | annotate |
| 2009-03-16 |
wenzelm |
2009-03-16 |
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
|
file | diff | annotate |
| 2009-03-12 |
wenzelm |
2009-03-12 |
renamed NameSpace.bind to NameSpace.define;
|
file | diff | annotate |
| 2009-03-07 |
wenzelm |
2009-03-07 |
moved Thm.def_name(_optional) to more_thm.ML;
moved old-style Thm.get_def to Drule.get_def;
|
file | diff | annotate |