| Mon, 28 Aug 2000 10:16:58 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 28 Aug 2000 09:32:51 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 25 Aug 2000 12:17:09 +0200 |
paulson |
added \trivlist...\endtrivlist to the "isabelle" environment
|
changeset |
files
|
| Fri, 25 Aug 2000 12:15:35 +0200 |
paulson |
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
|
changeset |
files
|
| Thu, 24 Aug 2000 12:39:42 +0200 |
paulson |
xsymbols for {| and |}
|
changeset |
files
|
| Thu, 24 Aug 2000 12:39:24 +0200 |
paulson |
xsymbols for leads-to and Join
|
changeset |
files
|
| Thu, 24 Aug 2000 11:14:21 +0200 |
paulson |
fixed strip_assums and assum_pairs, restoring them (essentially) to their
|
changeset |
files
|
| Thu, 24 Aug 2000 11:05:20 +0200 |
paulson |
added some xsymbols, and tidied
|
changeset |
files
|
| Thu, 24 Aug 2000 00:55:42 +0200 |
wenzelm |
more symbols;
|
changeset |
files
|
| Thu, 24 Aug 2000 00:54:54 +0200 |
wenzelm |
disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
|
changeset |
files
|
| Thu, 24 Aug 2000 00:53:53 +0200 |
wenzelm |
choosefrom: support easy settings;
|
changeset |
files
|
| Thu, 24 Aug 2000 00:53:23 +0200 |
wenzelm |
choosefrom: easy settings;
|
changeset |
files
|