| Wed, 17 Aug 2011 22:14:22 +0200 |
more systematic handling of parallel exceptions;
|
file | diff | annotate |
| Tue, 09 Aug 2011 23:54:17 +0200 |
rename_bvs now avoids introducing name clashes between schematic variables
|
file | diff | annotate |
| Wed, 13 Jul 2011 21:44:15 +0200 |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
file | diff | annotate |
| Mon, 11 Jul 2011 22:55:47 +0200 |
tuned signature -- corresponding to Scala version;
|
file | diff | annotate |
| Wed, 08 Jun 2011 15:56:57 +0200 |
more robust exception pattern General.Subscript;
|
file | diff | annotate |
| Wed, 20 Apr 2011 13:54:07 +0200 |
added Theory.nodes_of convenience;
|
file | diff | annotate |
| Sun, 17 Apr 2011 19:54:04 +0200 |
report Name_Space.declare/define, relatively to context;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:47:52 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Sat, 16 Apr 2011 13:48:45 +0200 |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file | diff | annotate |
| Thu, 03 Feb 2011 20:13:49 +0100 |
thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
|
file | diff | annotate |
| Thu, 03 Feb 2011 19:27:04 +0100 |
tuned comments;
|
file | diff | annotate |
| Mon, 20 Feb 2012 18:18:03 +0100 |
Jan finished his work
|
file | diff | annotate |
| Sun, 19 Feb 2012 10:03:51 +0100 |
protocol dmeindl, decomment Test_Isac
|
file | diff | annotate |
| Fri, 25 Feb 2011 13:26:45 +0100 |
buid Pur, HOL worked
|
file | diff | annotate |
| Fri, 25 Feb 2011 13:04:56 +0100 |
merged isabisac with Isabelle2011
|
file | diff | annotate |
| Thu, 28 Oct 2010 22:23:11 +0200 |
type attribute is derived concept outside the kernel;
|
file | diff | annotate |
| Mon, 25 Oct 2010 11:22:30 +0200 |
recovered some odd two-dimensional layout;
|
file | diff | annotate |
| Fri, 24 Sep 2010 15:53:13 +0200 |
modernized structure Ord_List;
|
file | diff | annotate |
| Wed, 25 Aug 2010 15:12:49 +0200 |
structure Thm: less pervasive names;
|
file | diff | annotate |
| Wed, 21 Jul 2010 13:53:39 +0200 |
added isac-hook in Pure/thm and isac-code
|
file | diff | annotate |
| Thu, 03 Jun 2010 23:17:57 +0200 |
eliminated ML structure alias;
|
file | diff | annotate |
| Wed, 02 Jun 2010 21:39:35 +0200 |
always unconstrain thm proofs;
|
file | diff | annotate |
| Wed, 19 May 2010 10:17:05 +0200 |
dropped legacy_unconstrainT
|
file | diff | annotate |
| Fri, 14 May 2010 19:53:36 +0200 |
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 |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
file | diff | annotate |
| Sun, 09 May 2010 22:06:24 +0200 |
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
|
file | diff | annotate |
| Sun, 09 May 2010 19:50:56 +0200 |
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
|
file | diff | annotate |
| Sun, 09 May 2010 19:15:21 +0200 |
just one version of Thm.unconstrainT, which affects all variables;
|
file | diff | annotate |
| Sat, 08 May 2010 16:53:53 +0200 |
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 |
tuned signature;
|
file | diff | annotate |
| Tue, 04 May 2010 14:38:59 +0200 |
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 |
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
|
file | diff | annotate |
| Mon, 03 May 2010 20:13:36 +0200 |
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 |
minor tuning of Thm.strip_shyps -- no longer pervasive;
|
file | diff | annotate |
| Mon, 03 May 2010 15:34:55 +0200 |
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 |
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 |
added Term.fold_atyps_sorts convenience;
|
file | diff | annotate |
| Sun, 21 Mar 2010 22:13:31 +0100 |
Logic.mk_of_sort convenience;
|
file | diff | annotate |
| Sat, 20 Mar 2010 17:33:11 +0100 |
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 |
modernized structure Term_Ord;
|
file | diff | annotate |
| Wed, 25 Nov 2009 09:13:46 +0100 |
normalized uncurry take/drop
|
file | diff | annotate |
| Tue, 24 Nov 2009 17:28:25 +0100 |
curried take/drop
|
file | diff | annotate |
| Sat, 21 Nov 2009 15:49:29 +0100 |
explicitly mark some legacy freeze operations;
|
file | diff | annotate |
| Mon, 16 Nov 2009 21:57:16 +0100 |
generalized procs for rewrite_proof: allow skeleton;
|
file | diff | annotate |
| Sun, 15 Nov 2009 15:14:28 +0100 |
tuned;
|
file | diff | annotate |
| Sun, 08 Nov 2009 18:43:42 +0100 |
adapted Theory_Data;
|
file | diff | annotate |
| Sun, 25 Oct 2009 13:04:06 +0100 |
make SML/NJ happy;
|
file | diff | annotate |
| Sat, 24 Oct 2009 20:54:08 +0200 |
maintain explicit name space kind;
|
file | diff | annotate |
| Sat, 24 Oct 2009 19:47:37 +0200 |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file | diff | annotate |
| Sat, 24 Oct 2009 19:20:03 +0200 |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file | diff | annotate |
| Wed, 21 Oct 2009 12:09:37 +0200 |
curried inter as canonical list operation (beware of argument order)
|
file | diff | annotate |
| Wed, 21 Oct 2009 08:14:38 +0200 |
dropped redundant gen_ prefix
|
file | diff | annotate |
| Tue, 20 Oct 2009 16:13:01 +0200 |
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 |
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 |
eliminated redundant bindings;
|
file | diff | annotate |
| Mon, 28 Sep 2009 20:52:05 +0200 |
fold_body_thms: pass pthm identifier;
|
file | diff | annotate |
| Mon, 28 Sep 2009 12:09:55 +0200 |
tuned internal source structure;
|
file | diff | annotate |
| Wed, 16 Sep 2009 21:14:08 +0200 |
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 |
lambda/cabs/all: named variants;
|
file | diff | annotate |
| Tue, 21 Jul 2009 20:37:32 +0200 |
simultaneous join_proofs;
|
file | diff | annotate |