| Sun, 07 Mar 2010 12:19:47 +0100 |
modernized structure Object_Logic;
|
file | diff | annotate |
| Sat, 06 Mar 2010 17:32:45 +0100 |
record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
|
file | diff | annotate |
| Sat, 06 Mar 2010 16:13:22 +0100 |
record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
|
file | diff | annotate |
| Wed, 03 Mar 2010 00:32:14 +0100 |
adapted to authentic syntax -- actual types are verbatim;
|
file | diff | annotate |
| Sun, 28 Feb 2010 23:51:31 +0100 |
more antiquotations;
|
file | diff | annotate |
| Sat, 27 Feb 2010 23:13:01 +0100 |
modernized structure Term_Ord;
|
file | diff | annotate |
| Thu, 25 Feb 2010 22:17:33 +0100 |
explicit @{type_syntax} markup;
|
file | diff | annotate |
| Sun, 21 Feb 2010 22:35:02 +0100 |
slightly more abstract syntax mark/unmark operations;
|
file | diff | annotate |
| Fri, 19 Feb 2010 22:06:01 +0100 |
tuned;
|
file | diff | annotate |
| Fri, 19 Feb 2010 21:31:14 +0100 |
authentic term syntax;
|
file | diff | annotate |
| Fri, 19 Feb 2010 16:11:45 +0100 |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
file | diff | annotate |
| Tue, 16 Feb 2010 20:41:52 +0100 |
simplified/clarified record print translations;
|
file | diff | annotate |
| Tue, 16 Feb 2010 16:42:18 +0100 |
eliminated camel case;
|
file | diff | annotate |
| Tue, 16 Feb 2010 16:40:16 +0100 |
tuned;
|
file | diff | annotate |
| Tue, 16 Feb 2010 16:03:06 +0100 |
simplified/clarified record translations;
|
file | diff | annotate |
| Tue, 16 Feb 2010 14:08:39 +0100 |
moved generic update_name to Pure syntax -- not specific to HOL/record;
|
file | diff | annotate |
| Tue, 16 Feb 2010 13:35:42 +0100 |
tuned;
|
file | diff | annotate |
| Tue, 16 Feb 2010 13:06:43 +0100 |
conceal internal record definitions;
|
file | diff | annotate |
| Mon, 15 Feb 2010 23:58:24 +0100 |
refined and exported record_info;
|
file | diff | annotate |
| Mon, 15 Feb 2010 22:40:03 +0100 |
modernized structures;
|
file | diff | annotate |
| Mon, 15 Feb 2010 22:24:19 +0100 |
modernized signature -- proper binding;
|
file | diff | annotate |
| Mon, 15 Feb 2010 20:32:21 +0100 |
tuned errors;
|
file | diff | annotate |
| Mon, 15 Feb 2010 20:01:07 +0100 |
formal markup of constants;
|
file | diff | annotate |
| Mon, 15 Feb 2010 18:50:16 +0100 |
eliminated old fold;
|
file | diff | annotate |
| Sun, 07 Feb 2010 19:33:34 +0100 |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file | diff | annotate |
| Mon, 21 Dec 2009 08:32:04 +0100 |
prefer prefix "iso" over potentially misleading "is"; tuned
|
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 |
| Mon, 16 Nov 2009 13:49:21 +0100 |
guard future proofs by Goal.future_enabled;
|
file | diff | annotate |
| Sat, 14 Nov 2009 09:31:54 +0100 |
clarified quick-and-dirty usage in record package;
|
file | diff | annotate |
| Wed, 11 Nov 2009 15:10:26 +0100 |
adding code equations for constructors
|
file | diff | annotate |
| Tue, 10 Nov 2009 16:11:43 +0100 |
substantial simplification restores code generation
|
file | diff | annotate |
| Sun, 08 Nov 2009 18:43:42 +0100 |
adapted Theory_Data;
|
file | diff | annotate |
| Mon, 02 Nov 2009 20:38:46 +0100 |
modernized structure Primitive_Defs;
|
file | diff | annotate |
| Sun, 01 Nov 2009 15:24:45 +0100 |
modernized structure Rule_Cases;
|
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 |
| Thu, 22 Oct 2009 13:48:06 +0200 |
map_range (and map_index) combinator
|
file | diff | annotate |
| Wed, 21 Oct 2009 16:57:57 +0200 |
merged
|
file | diff | annotate |
| Wed, 21 Oct 2009 16:53:00 +0200 |
removed "nitpick_const_simp" attribute from Record's "simps";
|
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:16:25 +0200 |
merged
|
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 |
| Tue, 20 Oct 2009 20:54:31 +0200 |
uniform use of Integer.min/max;
|
file | diff | annotate |
| Sat, 17 Oct 2009 21:14:08 +0200 |
tuned;
|
file | diff | annotate |
| Sat, 17 Oct 2009 20:37:38 +0200 |
removed separate record_quick_and_dirty_sensitive;
|
file | diff | annotate |
| Sat, 17 Oct 2009 20:15:59 +0200 |
simplified tactics;
|
file | diff | annotate |
| Sat, 17 Oct 2009 19:04:35 +0200 |
eliminated old List.foldr and OldTerm operations;
|
file | diff | annotate |
| Sat, 17 Oct 2009 18:14:47 +0200 |
removed unused names;
|
file | diff | annotate |
| Sat, 17 Oct 2009 18:01:24 +0200 |
misc tuning and simplification;
|
file | diff | annotate |
| Sat, 17 Oct 2009 16:58:03 +0200 |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file | diff | annotate |
| Sat, 17 Oct 2009 00:52:37 +0200 |
explicitly qualify Drule.standard;
|
file | diff | annotate |
| Thu, 15 Oct 2009 23:28:10 +0200 |
replaced String.concat by implode;
|
file | diff | annotate |
| Thu, 01 Oct 2009 14:11:28 +0200 |
avoid mixed l/r infixes, which do not work in some versions of SML;
|
file | diff | annotate |
| Thu, 01 Oct 2009 12:15:35 +0200 |
tuned;
|
file | diff | annotate |
| Thu, 01 Oct 2009 01:03:36 +0200 |
eliminated dead code, redundant bindings and parameters;
|
file | diff | annotate |
| Wed, 30 Sep 2009 00:27:19 +0200 |
made SML/NJ happy;
|
file | diff | annotate |
| Tue, 29 Sep 2009 23:14:57 +0200 |
removed dead/duplicate code;
|
file | diff | annotate |
| Tue, 29 Sep 2009 22:48:24 +0200 |
modernized Balanced_Tree;
|
file | diff | annotate |
| Tue, 29 Sep 2009 22:33:27 +0200 |
replaced meta_iffD2 by existing Drule.equal_elim_rule2;
|
file | diff | annotate |