Mon, 06 Nov 2000 22:56:07 +0100 |
wenzelm |
improved: 'induct' handle non-atomic goals;
|
changeset |
files
|
Mon, 06 Nov 2000 22:54:13 +0100 |
wenzelm |
make: open_parms argument;
|
changeset |
files
|
Mon, 06 Nov 2000 22:53:00 +0100 |
wenzelm |
RuleCases.make true;
|
changeset |
files
|
Mon, 06 Nov 2000 22:52:35 +0100 |
wenzelm |
added rewrite_goal_tac;
|
changeset |
files
|
Mon, 06 Nov 2000 22:50:50 +0100 |
wenzelm |
added typ_instance;
|
changeset |
files
|
Mon, 06 Nov 2000 22:50:01 +0100 |
wenzelm |
Sign.typ_instance;
|
changeset |
files
|
Mon, 06 Nov 2000 22:49:16 +0100 |
wenzelm |
inductive_atomize, inductive_rulify;
|
changeset |
files
|
Mon, 06 Nov 2000 22:48:42 +0100 |
wenzelm |
* Isar/HOL: method 'induct' now handles non-atomic goals; as a
|
changeset |
files
|
Mon, 06 Nov 2000 22:47:41 +0100 |
wenzelm |
tuned atomize_goal;
|
changeset |
files
|
Mon, 06 Nov 2000 18:28:22 +0100 |
paulson |
minor modifications for new Springer style
|
changeset |
files
|
Mon, 06 Nov 2000 16:43:01 +0100 |
paulson |
minor changes
|
changeset |
files
|
Mon, 06 Nov 2000 16:41:39 +0100 |
paulson |
auto update
|
changeset |
files
|