| Sun, 10 Aug 2014 15:45:06 +0200 |
wenzelm |
tuned -- avoid confusion with @{assert} for system failures (exception Fail);
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 21:23:21 +0100 |
wenzelm |
eliminated old-fashioned Global_Theory.add_thms(s);
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 20:55:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 16:37:35 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 16:24:48 +0100 |
wenzelm |
some localization;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:26:43 +0100 |
wenzelm |
eliminated some legacy operations;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 13:38:24 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 21:14:01 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 20:49:48 +0200 |
wenzelm |
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 10:03:13 +0100 |
huffman |
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
|
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
|
| 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
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 12:17:43 +0100 |
haftmann |
modernized structure Datatype_Aux
|
file |
diff |
annotate
|
| Wed, 02 Dec 2009 11:29:49 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 11:42:49 +0100 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:49:55 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 22:55:27 +0100 |
wenzelm |
Datatype.read_typ: standard argument order;
|
file |
diff |
annotate
|