| Thu, 25 Feb 2010 22:06:43 +0100 |
wenzelm |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 21:10:01 +0100 |
wenzelm |
adapted to authentic syntax;
|
file |
diff |
annotate
|
| Sun, 14 Feb 2010 00:26:48 +0100 |
wenzelm |
formal markup of constants;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:11:00 +0100 |
berghofe |
Injectivity / distinctness theorems are now used to simplify induction rules.
|
file |
diff |
annotate
|
| Wed, 02 Dec 2009 11:29:49 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
| base
|
| Mon, 30 Nov 2009 12:28:12 +0100 |
haftmann |
dropped some unused bindings
|
file |
diff |
annotate
| base
|
| 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
| base
|
| Fri, 27 Nov 2009 08:42:34 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML
|
file |
diff |
annotate
| base
|
| Fri, 27 Nov 2009 08:41:10 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
| base
|