Fri, 19 Jan 2007 22:08:04 +0100 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
changeset |
files
|
Fri, 19 Jan 2007 22:08:03 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
changeset |
files
|
Fri, 19 Jan 2007 22:08:01 +0100 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
changeset |
files
|
Fri, 19 Jan 2007 22:04:22 +0100 |
webertj |
interpreter for Finite_Set.finite added
|
changeset |
files
|
Fri, 19 Jan 2007 21:20:10 +0100 |
webertj |
reformatted to 80 chars/line
|
changeset |
files
|
Fri, 19 Jan 2007 15:13:47 +0100 |
chaieb |
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset.
|
changeset |
files
|
Fri, 19 Jan 2007 13:16:37 +0100 |
wenzelm |
adapted ML context operations;
|
changeset |
files
|
Fri, 19 Jan 2007 13:09:37 +0100 |
wenzelm |
added generic_theory_of;
|
changeset |
files
|
Fri, 19 Jan 2007 13:09:36 +0100 |
wenzelm |
added 'declaration' command;
|
changeset |
files
|
Fri, 19 Jan 2007 13:09:35 +0100 |
wenzelm |
added 'declaration' command;
|
changeset |
files
|
Fri, 19 Jan 2007 13:09:33 +0100 |
wenzelm |
adapted ML context operations;
|
changeset |
files
|