| Thu, 29 Dec 2011 18:27:17 +0100 |
wenzelm |
clarified timeit_msg;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 16:58:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 20:10:28 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 15:23:27 +0100 |
wenzelm |
eliminated some legacy operations;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
adapting exhaustive generators in record package
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2011 11:02:06 +0100 |
wenzelm |
simultaneous check;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 17:57:42 +0100 |
wenzelm |
sort assignment before simultaneous term_check, not isolated parse_term;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 15:18:39 +0100 |
wenzelm |
localized Record.decode_type: use standard Proof_Context.get_sort;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 17:57:37 +0200 |
wenzelm |
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 22:02:52 +0200 |
wenzelm |
clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 20:14:13 +0200 |
wenzelm |
tuned errors;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 13:31:12 +0200 |
wenzelm |
record package: proper configuration options;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 11:37:29 +0200 |
wenzelm |
just one copy of split_args;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
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
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Thu, 05 May 2011 10:47:31 +0200 |
bulwahn |
adding creation of exhaustive generators for records; simplifying dependencies in Main theory
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 12:58:13 +0200 |
wenzelm |
moved unparse material to syntax_phases.ML;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 10:59:43 +0200 |
wenzelm |
renamed Standard_Syntax to Syntax_Phases;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 23:14:41 +0200 |
wenzelm |
moved decode/parse operations to standard_syntax.ML;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2011 12:01:40 +0100 |
wenzelm |
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adaptions in generators using the common functions
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adapting record package to renaming of quickcheck's structures
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 19:44:59 +0100 |
wenzelm |
proper type variables with sorts;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 17:32:07 +0100 |
wenzelm |
recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 16:49:10 +0100 |
wenzelm |
export Record.get_hierarchy -- external tools typically need this information;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 15:37:49 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 15:29:17 +0100 |
wenzelm |
removed unreferenced identifiers;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:19:48 +0100 |
wenzelm |
standardized split_last/last_elem towards List.last;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:35:40 +0100 |
wenzelm |
just one HOLogic.mk_comp;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 13:09:08 +0100 |
wenzelm |
just one Term.dest_funT;
|
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
|
| Wed, 03 Nov 2010 10:51:40 +0100 |
wenzelm |
try_param_tac: plain user error appears more appropriate;
|
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
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 16:25:25 +0200 |
wenzelm |
misc tuning and simplification, notably theory data;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 16:59:37 +0200 |
haftmann |
re-added instantiation of type class random for records
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 16:35:23 +0200 |
haftmann |
tuned code
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 16:27:58 +0200 |
haftmann |
use extension constant as formal constructor of logical record type
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 15:29:41 +0200 |
haftmann |
authentic syntax allows simplification of type names
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 15:19:37 +0200 |
haftmann |
dropped make_/dest_ naming convention
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 15:17:44 +0200 |
haftmann |
formally integrated typecopy layer into record package
|
file |
diff |
annotate
|
| Fri, 13 Aug 2010 12:15:25 +0200 |
haftmann |
avoid variable name acc (cf. cs. 3142c1e21a0e)
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 13:56:02 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|