| 2007-12-08 |
wenzelm |
ML_OPTIONS="-H 1000" -- potentially works around GC core dump;
|
changeset |
files
|
| 2007-12-07 |
wenzelm |
added off-line parse;
|
changeset |
files
|
| 2007-12-07 |
wenzelm |
(alt)string: allow explicit character codes (as in ML);
|
changeset |
files
|
| 2007-12-07 |
wenzelm |
added nested 'Isabelle.command';
|
changeset |
files
|
| 2007-12-07 |
wenzelm |
updated;
|
changeset |
files
|
| 2007-12-07 |
wenzelm |
special_end: replaced Z by dot;
|
changeset |
files
|
| 2007-12-07 |
wenzelm |
output_prompt: CRITICAL;
|
changeset |
files
|
| 2007-12-07 |
haftmann |
declaration of instance parameter names
|
changeset |
files
|
| 2007-12-07 |
haftmann |
exported declare_names
|
changeset |
files
|
| 2007-12-07 |
haftmann |
new primrec
|
changeset |
files
|
| 2007-12-07 |
haftmann |
instantiation target rather than legacy instance
|
changeset |
files
|
| 2007-12-07 |
haftmann |
proper treatment of code theorems for primrec
|
changeset |
files
|
| 2007-12-07 |
haftmann |
dropped Instance.instantiate
|
changeset |
files
|
| 2007-12-07 |
krauss |
Adding "ex/Induction_Scheme.thy" to tests
|
changeset |
files
|
| 2007-12-07 |
krauss |
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
|
changeset |
files
|
| 2007-12-07 |
haftmann |
tuned further
|
changeset |
files
|
| 2007-12-06 |
wenzelm |
renamed ML_PID to PID;
|
changeset |
files
|
| 2007-12-06 |
nipkow |
R&F: added sgn lemma
|
changeset |
files
|
| 2007-12-06 |
haftmann |
temporary code generator work arounds
|
changeset |
files
|
| 2007-12-06 |
haftmann |
fixed slip
|
changeset |
files
|
| 2007-12-06 |
haftmann |
-authentic primrec
|
changeset |
files
|
| 2007-12-06 |
haftmann |
dropped legacy bindings
|
changeset |
files
|
| 2007-12-06 |
haftmann |
authentic primrec
|
changeset |
files
|
| 2007-12-06 |
haftmann |
dropped void space
|
changeset |
files
|
| 2007-12-06 |
haftmann |
added new primrec package
|
changeset |
files
|
| 2007-12-06 |
krauss |
load sum_tree.ML
|
changeset |
files
|
| 2007-12-06 |
krauss |
factored out handling of sum types again
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
added test_markup;
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
moved basic test_markup to isabelle_process.ML;
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
added channels;
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
check persistent sessions;
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| 2007-12-05 |
wenzelm |
removed -e flag from most sessions;
|
changeset |
files
|
| 2007-12-05 |
obua |
instance int,real :: lordered_ring
|
changeset |
files
|
| 2007-12-05 |
krauss |
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
|
changeset |
files
|
| 2007-12-05 |
haftmann |
tuned class parts
|
changeset |
files
|
| 2007-12-05 |
haftmann |
dropped Classpackage.thy
|
changeset |
files
|
| 2007-12-05 |
haftmann |
tuned
|
changeset |
files
|
| 2007-12-05 |
haftmann |
added parser for multi_arity
|
changeset |
files
|
| 2007-12-05 |
haftmann |
added constrain_thm
|
changeset |
files
|
| 2007-12-05 |
haftmann |
canonical instantiation
|
changeset |
files
|
| 2007-12-05 |
haftmann |
map_product and fold_product
|
changeset |
files
|
| 2007-12-05 |
haftmann |
interface and distinct simproc tuned
|
changeset |
files
|
| 2007-12-05 |
haftmann |
improved
|
changeset |
files
|
| 2007-12-05 |
haftmann |
interpretation of typedefs
|
changeset |
files
|
| 2007-12-05 |
haftmann |
simplified infrastructure for code generator operational equality
|
changeset |
files
|
| 2007-12-05 |
haftmann |
added something about instantiation target
|
changeset |
files
|
| 2007-12-05 |
kleing |
switch poly to 5.1, removed -e flag from most sessions
|
changeset |
files
|
| 2007-12-05 |
kleing |
switch at-poly main to poly 5.1
|
changeset |
files
|
| 2007-12-05 |
kleing |
make mac-poly non-experimental
|
changeset |
files
|
| 2007-12-05 |
kleing |
make at64 non-experimental
|
changeset |
files
|
| 2007-12-04 |
wenzelm |
Isabelle process wrapper -- interaction via external program.
|
changeset |
files
|
| 2007-12-04 |
wenzelm |
Toplevel.loop: explicit argument for secure loop, no warning on quit;
|
changeset |
files
|
| 2007-12-04 |
wenzelm |
added Isar.secure_main;
|
changeset |
files
|
| 2007-12-04 |
wenzelm |
added Tools/isabelle_process.ML;
|
changeset |
files
|
| 2007-12-04 |
wenzelm |
isabelle process: replaced option -p by -W (process wrapper);
|
changeset |
files
|
| 2007-12-04 |
wenzelm |
replaced option -p by -W (process wrapper);
|
changeset |
files
|
| 2007-12-04 |
wenzelm |
\<chi> is now considered a letter;
|
changeset |
files
|