| Fri, 02 Feb 2001 22:21:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 02 Feb 2001 22:20:43 +0100 |
wenzelm |
module setup;
|
changeset |
files
|
| Fri, 02 Feb 2001 22:20:09 +0100 |
wenzelm |
use hol_simplify;
|
changeset |
files
|
| Fri, 02 Feb 2001 22:19:52 +0100 |
wenzelm |
use hol_rewrite_cterm;
|
changeset |
files
|
| Fri, 02 Feb 2001 22:19:23 +0100 |
wenzelm |
added hol_simplify, hol_rewrite_cterm;
|
changeset |
files
|
| Fri, 02 Feb 2001 22:19:02 +0100 |
wenzelm |
split = split_conv (for compatibility);
|
changeset |
files
|
| Fri, 02 Feb 2001 22:18:10 +0100 |
wenzelm |
added hidden internal_split constant;
|
changeset |
files
|
| Fri, 02 Feb 2001 22:17:31 +0100 |
wenzelm |
isatool convert;
|
changeset |
files
|
| Fri, 02 Feb 2001 11:42:36 +0100 |
paulson |
new theorem fib_mult_eq_setsum
|
changeset |
files
|
| Fri, 02 Feb 2001 00:31:39 +0100 |
oheimb |
little bugfixes; added induct_thm_tac
|
changeset |
files
|
| Thu, 01 Feb 2001 21:28:23 +0100 |
wenzelm |
moved to Product_Type_lemmas.ML
|
changeset |
files
|
| Thu, 01 Feb 2001 20:56:21 +0100 |
oheimb |
added translations for bind_thm and val
|
changeset |
files
|
| Thu, 01 Feb 2001 20:53:13 +0100 |
oheimb |
converted to Isar, simplifying recursion on class hierarchy
|
changeset |
files
|
| Thu, 01 Feb 2001 20:51:48 +0100 |
oheimb |
converted to Isar therory, adding attributes complete_split and split_format
|
changeset |
files
|
| Thu, 01 Feb 2001 20:51:13 +0100 |
wenzelm |
converted to new-style theories;
|
changeset |
files
|