| 2011-06-27 |
wenzelm |
2011-06-27 |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
file | diff | annotate |
| 2011-06-09 |
wenzelm |
2011-06-09 |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file | diff | annotate |
| 2011-06-09 |
wenzelm |
2011-06-09 |
clarified special incr_type_indexes;
|
file | diff | annotate |
| 2011-06-09 |
wenzelm |
2011-06-09 |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file | diff | annotate |
| 2011-04-23 |
wenzelm |
2011-04-23 |
hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
|
file | diff | annotate |
| 2010-11-26 |
wenzelm |
2010-11-26 |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file | diff | annotate |
| 2010-09-20 |
wenzelm |
2010-09-20 |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file | diff | annotate |
| 2010-08-25 |
wenzelm |
2010-08-25 |
structure Thm: less pervasive names;
|
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 Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
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 |
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def;
modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
|
file | diff | annotate |
| 2010-03-22 |
wenzelm |
2010-03-22 |
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
|
file | diff | annotate |
| 2010-03-22 |
wenzelm |
2010-03-22 |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
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-19 |
wenzelm |
2010-02-19 |
moved ancient Drule.get_def to OldGoals.get_def;
|
file | diff | annotate |
| 2010-02-07 |
wenzelm |
2010-02-07 |
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-11-21 |
wenzelm |
2009-11-21 |
explicitly mark some legacy freeze operations;
|
file | diff | annotate |
| 2009-11-12 |
wenzelm |
2009-11-12 |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file | diff | annotate |
| 2009-11-02 |
wenzelm |
2009-11-02 |
modernized structure Simple_Syntax;
|
file | diff | annotate |
| 2009-10-28 |
wenzelm |
2009-10-28 |
Drule.store: proper binding;
conceal internal bindings;
|
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-17 |
wenzelm |
2009-10-17 |
legacy Drule.standard is no longer pervasive;
|
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 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| 2009-07-02 |
wenzelm |
2009-07-02 |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
file | diff | annotate |
| 2009-03-16 |
wenzelm |
2009-03-16 |
refined is_norm_hhf: reject beta-redexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
|
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 |
| 2009-01-21 |
haftmann |
2009-01-21 |
binding replaces bstring
|
file | diff | annotate |
| 2009-01-04 |
wenzelm |
2009-01-04 |
added comp_no_flatten;
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file | diff | annotate |
| 2008-10-31 |
berghofe |
2008-10-31 |
Theorem "_" is now stored with open derivation.
|
file | diff | annotate |
| 2008-10-23 |
wenzelm |
2008-10-23 |
renamed Thm.get_axiom_i to Thm.axiom;
|
file | diff | annotate |
| 2008-10-16 |
wenzelm |
2008-10-16 |
added rules for sort_constraint, include in norm_hhf_eqs;
tuned;
|
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-06-23 |
wenzelm |
2008-06-23 |
Logic.implies;
|
file | diff | annotate |
| 2008-06-19 |
wenzelm |
2008-06-19 |
moved add_used to Isar/rule_insts.ML;
|
file | diff | annotate |
| 2008-06-16 |
wenzelm |
2008-06-16 |
removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);
|
file | diff | annotate |
| 2008-06-11 |
wenzelm |
2008-06-11 |
qualified types_sorts, read_insts etc.;
|
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-15 |
wenzelm |
2008-04-15 |
Thm.forall_elim_var(s);
|
file | diff | annotate |
| 2008-04-12 |
wenzelm |
2008-04-12 |
rep_cterm/rep_thm: no longer dereference theory_ref;
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file | diff | annotate |
| 2008-03-29 |
wenzelm |
2008-03-29 |
certify wrt. dynamic context;
functional store_thm (wrt. thread data);
|
file | diff | annotate |
| 2008-03-27 |
wenzelm |
2008-03-27 |
eliminated theory ProtoPure;
|
file | diff | annotate |
| 2007-11-27 |
berghofe |
2007-11-27 |
Better error messages for cterm_instantiate.
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
tuned;
|
file | diff | annotate |
| 2007-10-10 |
wenzelm |
2007-10-10 |
improved abs_def: only abstract over outermost (unique) Vars;
|
file | diff | annotate |
| 2007-10-04 |
wenzelm |
2007-10-04 |
replaced literal 'a by Name.aT;
|
file | diff | annotate |
| 2007-08-24 |
paulson |
2007-08-24 |
new derived rule: incr_type_indexes
|
file | diff | annotate |
| 2007-08-13 |
wenzelm |
2007-08-13 |
SimpleSyntax.read_prop;
|
file | diff | annotate |
| 2007-07-29 |
wenzelm |
2007-07-29 |
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
moved Drule.is_dummy_thm to Thm.is_dummy;
|
file | diff | annotate |
| 2007-07-27 |
wenzelm |
2007-07-27 |
added dummy_thm, is_dummy_thm;
|
file | diff | annotate |
| 2007-07-04 |
wenzelm |
2007-07-04 |
added binop_cong_rule;
|
file | diff | annotate |
| 2007-07-03 |
wenzelm |
2007-07-03 |
tuned rotate_prems;
tuned comments;
|
file | diff | annotate |
| 2007-06-20 |
paulson |
2007-06-20 |
A more robust flexflex_unique
|
file | diff | annotate |
| 2007-06-19 |
wenzelm |
2007-06-19 |
added with_subgoal;
|
file | diff | annotate |
| 2007-05-31 |
wenzelm |
2007-05-31 |
simplified/unified list fold;
|
file | diff | annotate |
| 2007-05-11 |
wenzelm |
2007-05-11 |
proper type for fun/arg_cong_rule;
|
file | diff | annotate |
| 2007-05-11 |
wenzelm |
2007-05-11 |
added fun/arg_cong_rule;
|
file | diff | annotate |