| 2005-09-06 |
huffman |
class instances for nonstandard types
|
changeset |
files
|
| 2005-09-06 |
huffman |
transfer principle tactic
|
changeset |
files
|
| 2005-09-06 |
huffman |
generic nonstandard type constructor
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-06 |
huffman |
fix proof
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-06 |
huffman |
reimplement Filter.thy with locales
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
removed some ML files in Modelcheck/;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
updated;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
axclass: no longer bind "cI";
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
deprecated old-style infix declarations, which mix name and syntax;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
tuned msg;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
AList.defined;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
name space prefix is now "c_class" instead of just "c";
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
proper treatment of polymorphic sets;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
tuned comments;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
make LocalesTest last, because it sets funny flags;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
avoid old-style infixes;
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
axclass: name space prefix is now "c_class" instead of just "c";
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
axclass: name space prefix is now "c_class" instead of just "c";
|
changeset |
files
|
| 2005-09-06 |
webertj |
unnecessary parentheses removed
|
changeset |
files
|
| 2005-09-06 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-06 |
haftmann |
introduced some new-style AList operations
|
changeset |
files
|
| 2005-09-06 |
haftmann |
eliminated 1 call to polyEq
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
updated;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
obsolete;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
added assert, command;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
tuned check_text;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
chapter/section/subsection/subsubsection/text: optional locale specification;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
markup commands: optional locale specification;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
add_chapter/section/subsection/subsubsection/text: optional locale specification;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
curried_lookup/update;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
Markup commands 'chapter' .. 'text' support optional locale specification;
|
changeset |
files
|
| 2005-09-05 |
wenzelm |
removed duplicate theorems;
|
changeset |
files
|
| 2005-09-05 |
haftmann |
introduced binding priority 1 for linear combinators etc.
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
tuned method;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
obsolete;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
obsolete (see Cube.thy);
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
tuned msg;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
uses ("LCF_lemmas.ML");
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
removed fix.thy, pair.thy, simpdata.ML;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
setmp print_mode []; more robust outer syntax; tuned;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
simplified oracle;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
use Check.ML;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
fixed ML errors;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
|
changeset |
files
|
| 2005-09-03 |
wenzelm |
deprecated non-Isar theory file format;
|
changeset |
files
|