Thu, 17 Aug 2000 10:32:44 +0200 |
wenzelm |
index tokens;
|
changeset |
files
|
Thu, 17 Aug 2000 10:32:20 +0200 |
wenzelm |
cases/induct method: 'opaque' by default; added 'open' option;
|
changeset |
files
|
Thu, 17 Aug 2000 10:31:43 +0200 |
wenzelm |
updated;
|
changeset |
files
|
Thu, 17 Aug 2000 10:31:10 +0200 |
wenzelm |
renamed 'RS' to 'THEN';
|
changeset |
files
|
Thu, 17 Aug 2000 10:29:50 +0200 |
wenzelm |
fixed lbrace, rbrace;
|
changeset |
files
|
Thu, 17 Aug 2000 10:29:23 +0200 |
wenzelm |
Isar/Pure: renamed 'RS' attribute to 'THEN';
|
changeset |
files
|
Wed, 16 Aug 2000 18:10:15 +0200 |
nipkow |
Fixed completeness bug in simplifier: congruence rules could preclude
|
changeset |
files
|
Wed, 16 Aug 2000 10:25:02 +0200 |
paulson |
major sharpening of stable_project_transient
|
changeset |
files
|
Wed, 16 Aug 2000 10:23:25 +0200 |
paulson |
new (unused) lemma
|
changeset |
files
|
Wed, 16 Aug 2000 10:22:41 +0200 |
paulson |
new thm and simprule Compl_Diff_eq
|
changeset |
files
|
Mon, 14 Aug 2000 18:49:35 +0200 |
wenzelm |
added conversion.tex;
|
changeset |
files
|
Mon, 14 Aug 2000 18:49:23 +0200 |
wenzelm |
moved tactic emulation methods here;
|
changeset |
files
|
Mon, 14 Aug 2000 18:47:32 +0200 |
wenzelm |
added 'declare' command;
|
changeset |
files
|
Mon, 14 Aug 2000 18:45:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 14 Aug 2000 18:45:31 +0200 |
wenzelm |
updated;
|
changeset |
files
|