Tue, 10 Jul 2007 23:29:41 +0200 |
wenzelm |
simplified funpow, untabify;
|
changeset |
files
|
Tue, 10 Jul 2007 23:29:38 +0200 |
wenzelm |
added Thy/thy_edit.ML;
|
changeset |
files
|
Tue, 10 Jul 2007 23:29:35 +0200 |
wenzelm |
added some markup for outer syntax;
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:57 +0200 |
haftmann |
clarified merge of module names
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:56 +0200 |
haftmann |
now a monolithic module
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:54 +0200 |
haftmann |
now works with SML/NJ
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:53 +0200 |
haftmann |
tuned
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:52 +0200 |
haftmann |
improvement for code names
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:51 +0200 |
haftmann |
removed proof dependency on transitivity theorems
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:50 +0200 |
haftmann |
moved lfp_induct2 here
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:49 +0200 |
haftmann |
clarified import
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:47 +0200 |
haftmann |
moved lfp_induct2 to Relation.thy
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:45 +0200 |
haftmann |
moved some finite lemmas here
|
changeset |
files
|
Tue, 10 Jul 2007 17:30:43 +0200 |
haftmann |
moved finite lemmas to Finite_Set.thy
|
changeset |
files
|
Tue, 10 Jul 2007 16:46:37 +0200 |
wenzelm |
added print_mode setup (from pretty.ML);
|
changeset |
files
|