| 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
|
| Tue, 27 Jul 2010 17:09:35 +0200 |
haftmann |
delete structure Basic_Record; avoid `record` in names in structure Record
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| Sat, 19 Jun 2010 09:50:30 +0200 |
haftmann |
more binding; avoid arcane Rep and Abs prefixes
|
file |
diff |
annotate
|
| Sat, 19 Jun 2010 09:14:06 +0200 |
haftmann |
cleanup of typecopy package
|
file |
diff |
annotate
|
| Sat, 29 May 2010 19:46:29 +0200 |
wenzelm |
explicit markup for forked goals, as indicated by Goal.fork;
|
file |
diff |
annotate
|
| Wed, 26 May 2010 16:05:25 +0200 |
haftmann |
dropped legacy theorem bindings
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 19:58:04 +0200 |
wenzelm |
modernized type abbreviations;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 21:24:00 +0200 |
wenzelm |
more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 18:09:22 +0200 |
wenzelm |
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 16:58:12 +0200 |
wenzelm |
modernized treatment of sort constraints in specification;
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 16:15:19 +0200 |
krauss |
record package: corrected sort handling in type translations to avoid crashes when default sort is changed.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 21:38:38 +0100 |
wenzelm |
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 18:07:21 +0100 |
wenzelm |
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:43:04 +0100 |
wenzelm |
global typedef;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 17:32:45 +0100 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
adapted to authentic syntax -- actual types are verbatim;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:17:33 +0100 |
wenzelm |
explicit @{type_syntax} markup;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 22:06:01 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 21:31:14 +0100 |
wenzelm |
authentic term syntax;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 16:11:45 +0100 |
wenzelm |
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 |
wenzelm |
simplified/clarified record print translations;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 16:42:18 +0100 |
wenzelm |
eliminated camel case;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 16:40:16 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 16:03:06 +0100 |
wenzelm |
simplified/clarified record translations;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 14:08:39 +0100 |
wenzelm |
moved generic update_name to Pure syntax -- not specific to HOL/record;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 13:35:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 13:06:43 +0100 |
wenzelm |
conceal internal record definitions;
|
file |
diff |
annotate
|