| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:45:41 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 15:03:55 +0200 |
wenzelm |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:56:08 +0200 |
wenzelm |
clarified special incr_type_indexes;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 19:41:53 +0200 |
wenzelm |
hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:29:41 +0100 |
wenzelm |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 15:12:49 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:41:32 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 20:13:36 +0200 |
wenzelm |
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 23:09:32 +0200 |
wenzelm |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 15:20:31 +0100 |
wenzelm |
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 19:29:11 +0100 |
wenzelm |
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
|
| Mon, 22 Mar 2010 00:48:56 +0100 |
wenzelm |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 20:39:48 +0100 |
wenzelm |
moved ancient Drule.get_def to OldGoals.get_def;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:33:34 +0100 |
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
|
| Sat, 21 Nov 2009 15:49:29 +0100 |
wenzelm |
explicitly mark some legacy freeze operations;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:34:59 +0100 |
wenzelm |
modernized structure Simple_Syntax;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:25:26 +0100 |
wenzelm |
Drule.store: proper binding;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 00:53:18 +0200 |
wenzelm |
legacy Drule.standard is no longer pervasive;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 21:26:18 +0200 |
wenzelm |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 23:39:44 +0100 |
wenzelm |
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
|
| Sat, 07 Mar 2009 22:04:59 +0100 |
wenzelm |
moved Thm.def_name(_optional) to more_thm.ML;
|
file |
diff |
annotate
|