Sun, 30 Jul 2000 12:50:51 +0200 |
wenzelm |
ObtainFun (generalized existence reasoning);
|
changeset |
files
|
Sun, 30 Jul 2000 12:50:33 +0200 |
wenzelm |
ThmDeps.enable;
|
changeset |
files
|
Sun, 30 Jul 2000 12:50:07 +0200 |
wenzelm |
added sign_of_cterm;
|
changeset |
files
|
Sun, 30 Jul 2000 12:48:55 +0200 |
wenzelm |
Logic.goal_const;
|
changeset |
files
|
Fri, 28 Jul 2000 16:08:41 +0200 |
wenzelm |
replaced "Sessions" by "Root";
|
changeset |
files
|
Fri, 28 Jul 2000 16:02:51 +0200 |
nipkow |
apply. -> by
|
changeset |
files
|
Fri, 28 Jul 2000 13:04:59 +0200 |
nipkow |
* HOL/While
|
changeset |
files
|
Thu, 27 Jul 2000 18:27:25 +0200 |
wenzelm |
added theory While;
|
changeset |
files
|
Thu, 27 Jul 2000 18:27:09 +0200 |
wenzelm |
export has_internal;
|
changeset |
files
|
Thu, 27 Jul 2000 18:25:55 +0200 |
wenzelm |
added thm_deps;
|
changeset |
files
|
Thu, 27 Jul 2000 18:25:44 +0200 |
wenzelm |
added enter_forward_proof;
|
changeset |
files
|
Thu, 27 Jul 2000 18:25:28 +0200 |
wenzelm |
export write_graph;
|
changeset |
files
|