| Sat, 17 Sep 2005 12:18:07 +0200 |
wenzelm |
added auto_fix (from proof.ML);
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:06 +0200 |
wenzelm |
export put_facts;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:05 +0200 |
wenzelm |
interpretation: use goal commands without target -- no storing of results;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:04 +0200 |
wenzelm |
theorem(_i): empty target;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:03 +0200 |
wenzelm |
pretty_thm_aux: observe asms context;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:00 +0200 |
wenzelm |
Cube: converted to Isar, use locales;
|
changeset |
files
|
| Sat, 17 Sep 2005 11:49:29 +0200 |
obua |
1) mapped .. and == constants
|
changeset |
files
|
| Sat, 17 Sep 2005 01:50:01 +0200 |
huffman |
use interpretation command
|
changeset |
files
|
| Fri, 16 Sep 2005 23:55:23 +0200 |
huffman |
add HOLCF entries for pcpodef, cont_proc, fixrec;
|
changeset |
files
|
| Fri, 16 Sep 2005 23:01:29 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Fri, 16 Sep 2005 21:02:15 +0200 |
obua |
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
|
changeset |
files
|
| Fri, 16 Sep 2005 20:30:44 +0200 |
huffman |
add header
|
changeset |
files
|
| Fri, 16 Sep 2005 16:07:22 +0200 |
ballarin |
tuned
|
changeset |
files
|