| Thu, 28 Oct 2010 22:23:11 +0200 |
wenzelm |
type attribute is derived concept outside the kernel;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 11:22:30 +0200 |
wenzelm |
recovered some odd two-dimensional layout;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 15:53:13 +0200 |
wenzelm |
modernized structure Ord_List;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 15:12:49 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 23:17:57 +0200 |
wenzelm |
eliminated ML structure alias;
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 21:39:35 +0200 |
wenzelm |
always unconstrain thm proofs;
|
file |
diff |
annotate
|
| Wed, 19 May 2010 10:17:05 +0200 |
haftmann |
dropped legacy_unconstrainT
|
file |
diff |
annotate
|
| Fri, 14 May 2010 19:53:36 +0200 |
wenzelm |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
file |
diff |
annotate
|
| Thu, 13 May 2010 21:36:38 +0200 |
wenzelm |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 22:06:24 +0200 |
wenzelm |
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 19:50:56 +0200 |
wenzelm |
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 19:15:21 +0200 |
wenzelm |
just one version of Thm.unconstrainT, which affects all variables;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 16:53:53 +0200 |
wenzelm |
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
|
| Sat, 08 May 2010 16:24:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 14:38:59 +0200 |
wenzelm |
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
|
file |
diff |
annotate
|
| Tue, 04 May 2010 11:02:50 +0200 |
wenzelm |
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
|
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
|
| Mon, 03 May 2010 16:26:47 +0200 |
wenzelm |
minor tuning of Thm.strip_shyps -- no longer pervasive;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 15:34:55 +0200 |
wenzelm |
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
|
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:47:57 +0100 |
wenzelm |
added Term.fold_atyps_sorts convenience;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 22:13:31 +0100 |
wenzelm |
Logic.mk_of_sort convenience;
|
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
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sat, 21 Nov 2009 15:49:29 +0100 |
wenzelm |
explicitly mark some legacy freeze operations;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 21:57:16 +0100 |
wenzelm |
generalized procs for rewrite_proof: allow skeleton;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 15:14:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:04:06 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 20:54:08 +0200 |
wenzelm |
maintain explicit name space kind;
|
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, 24 Oct 2009 19:20:03 +0200 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:09:37 +0200 |
haftmann |
curried inter as canonical list operation (beware of argument order)
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 14:27:50 +0200 |
wenzelm |
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
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 20:52:05 +0200 |
wenzelm |
fold_body_thms: pass pthm identifier;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 12:09:55 +0200 |
wenzelm |
tuned internal source structure;
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 21:14:08 +0200 |
wenzelm |
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
|
| Sun, 26 Jul 2009 13:12:53 +0200 |
wenzelm |
lambda/cabs/all: named variants;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 20:37:32 +0200 |
wenzelm |
simultaneous join_proofs;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 10:24:57 +0200 |
wenzelm |
prefer simultaneous join -- for improved scheduling;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2009 18:42:05 +0200 |
wenzelm |
support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 23:11:40 +0200 |
wenzelm |
tuned/modernized Envir.subst_XXX;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 22:58:45 +0200 |
wenzelm |
tuned incr_indexes;
|
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 22:42:27 +0200 |
wenzelm |
clarified strip_shyps: proper type witnesses for present sorts;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 20:36:38 +0200 |
wenzelm |
clarified Thm.of_class/of_sort/class_triv;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 19:58:52 +0200 |
wenzelm |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 22:17:08 +0200 |
wenzelm |
strip_shyps: remove top sort, which is logically insignificant;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 20:55:44 +0200 |
wenzelm |
added pro-forma proof constructor Inclass;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2009 16:54:17 +0100 |
wenzelm |
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 22:56:17 +0100 |
wenzelm |
status_of: need to include local promises as well!
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 21:24:53 +0100 |
wenzelm |
display derivation status of thms;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 12:10:42 +0100 |
wenzelm |
eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 23:52:30 +0100 |
wenzelm |
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
|
| Thu, 12 Mar 2009 11:10:02 +0100 |
wenzelm |
renamed NameSpace.bind to NameSpace.define;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:04:59 +0100 |
wenzelm |
moved Thm.def_name(_optional) to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 19:48:02 +0100 |
wenzelm |
Thm.add_oracle interface: replaced old bstring by binding;
|
file |
diff |
annotate
|
| Tue, 27 Jan 2009 00:42:12 +0100 |
wenzelm |
thm_proof: replaced lazy by composed futures;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 21:47:02 +0100 |
wenzelm |
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 16:54:55 +0100 |
wenzelm |
added pending_groups -- accumulates task groups of local derivations only;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:17 +0100 |
wenzelm |
use regular Term.add_XXX etc.;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 00:09:01 +0100 |
wenzelm |
renamed force_proof to join_proof;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 20:38:40 +0100 |
wenzelm |
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 08:05:14 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 00:23:37 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:02:56 +0100 |
wenzelm |
future proofs: pass actual futures to facilitate composite computations;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Sun, 23 Nov 2008 17:25:56 +0100 |
wenzelm |
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 22:25:36 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 18:25:52 +0100 |
wenzelm |
added force_proofs;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 23:17:13 +0100 |
wenzelm |
tuned promise/fullfill;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 22:12:43 +0100 |
wenzelm |
put_name/thm_proof: promises are filled with fulfilled proofs;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:25 +0100 |
wenzelm |
refined notion of derivation, consiting of promises and proof_body;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 15:28:05 +0200 |
wenzelm |
renamed get_axiom_i to axiom, removed obsolete get_axiom;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 16:53:10 +0200 |
wenzelm |
join results in isolation;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:33 +0200 |
wenzelm |
added weaken_sorts;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:18:18 +0200 |
wenzelm |
renamed promise to future, tuned related interfaces;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:00:00 +0200 |
wenzelm |
more precise join_futures, improved termination;
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 22:02:44 +0200 |
wenzelm |
export explicit joint_futures, removed Theory.at_end hook;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 12:42:35 +0200 |
wenzelm |
join earlier promises first;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 12:23:44 +0200 |
wenzelm |
promise_result: enforce strictly sequential dependencies, via serial numbers;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 18:18:05 +0200 |
wenzelm |
Future.release_results;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 15:20:37 +0200 |
wenzelm |
promise: include check into future body, i.e. joined results are always valid;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 20:34:19 +0200 |
wenzelm |
simplified promise;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 14:35:02 +0200 |
wenzelm |
abtract types: plain datatype with opaque signature matching;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 13:21:13 +0200 |
wenzelm |
explicit type OrdList.T;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 15:48:52 +0200 |
wenzelm |
added dest_deriv, removed external type deriv;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 15:26:14 +0200 |
wenzelm |
type thm: fully internal derivation, no longer exported;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 14:06:56 +0200 |
wenzelm |
added deriv.ML: Abstract derivations based on raw proof terms.
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:49 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:47 +0200 |
berghofe |
eq_assumption now uses aeconv instead of aconv.
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:19 +0200 |
wenzelm |
Theory.eq_thy;
|
file |
diff |
annotate
|
| Sun, 13 Apr 2008 16:40:06 +0200 |
wenzelm |
simplified handling of sorts, removed unnecessary universal witness;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:45 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Mon, 21 Jan 2008 14:18:49 +0100 |
berghofe |
Removed Logic.auto_rename.
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:45 +0200 |
wenzelm |
compress: proper check_thy;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 16:28:22 +0200 |
wenzelm |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:59:21 +0200 |
berghofe |
Added function norm_proof for normalizing the proof term
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:52:05 +0200 |
wenzelm |
thm tag: Markup.property list;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:38 +0200 |
wenzelm |
added type conv;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:42 +0200 |
wenzelm |
added eta_long_conversion;
|
file |
diff |
annotate
|
| Fri, 08 Jun 2007 18:13:58 +0200 |
berghofe |
Adapted Proofterm.bicompose_proof to Larry's changes in
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:55 +0200 |
wenzelm |
added dest_fun/fun2/arg1;
|
file |
diff |
annotate
|