| Wed, 19 Feb 2014 10:21:02 +0100 |
traytel |
removed not anymore used constants and theorems
|
changeset |
files
|
| Wed, 19 Feb 2014 09:50:50 +0100 |
traytel |
simplifications of internal codatatype construction
|
changeset |
files
|
| Wed, 19 Feb 2014 08:34:34 +0100 |
blanchet |
adapted Nitpick to 'primrec' refactoring
|
changeset |
files
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
changeset |
files
|
| Wed, 19 Feb 2014 08:34:32 +0100 |
blanchet |
rewrote a small portion of code to avoid dependency on low-level constant
|
changeset |
files
|
| Wed, 19 Feb 2014 08:33:59 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 19 Feb 2014 17:16:40 +1100 |
kleing |
provide more automation for type definitions (makes book exercises easier)
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:59 +0100 |
blanchet |
prepare two-stage 'primrec' setup
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:58 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:57 +0100 |
blanchet |
removed deadcode
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:55 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 18 Feb 2014 17:52:28 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 18 Feb 2014 17:52:27 +0100 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
changeset |
files
|
| Tue, 18 Feb 2014 23:03:49 +0100 |
kuncar |
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
|
changeset |
files
|
| Tue, 18 Feb 2014 23:03:47 +0100 |
kuncar |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
changeset |
files
|
| Tue, 18 Feb 2014 21:00:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 18 Feb 2014 20:50:07 +0100 |
wenzelm |
more markup;
|
changeset |
files
|
| Tue, 18 Feb 2014 20:37:45 +0100 |
wenzelm |
proper term equality;
|
changeset |
files
|
| Tue, 18 Feb 2014 20:32:58 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Tue, 18 Feb 2014 20:20:42 +0100 |
wenzelm |
more uniform treatment of dockables and their standard actions;
|
changeset |
files
|
| Tue, 18 Feb 2014 19:00:13 +0100 |
wenzelm |
standardized action and panel names;
|
changeset |
files
|
| Tue, 18 Feb 2014 18:51:03 +0100 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Tue, 18 Feb 2014 18:43:47 +0100 |
wenzelm |
prefer concrete list append;
|
changeset |
files
|
| Tue, 18 Feb 2014 18:43:31 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 18 Feb 2014 18:29:02 +0100 |
wenzelm |
more standard names for protocol and markup elements;
|
changeset |
files
|
| Tue, 18 Feb 2014 17:26:13 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 18 Feb 2014 17:03:12 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 18 Feb 2014 16:34:02 +0100 |
wenzelm |
generic markup for embedded languages;
|
changeset |
files
|
| Tue, 18 Feb 2014 15:38:50 +0100 |
wenzelm |
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
|
changeset |
files
|