| 2009-07-04 |
chaieb |
merged
|
changeset |
files
|
| 2009-07-04 |
chaieb |
merged
|
changeset |
files
|
| 2009-07-02 |
chaieb |
Gettring rid of sorts hyps
|
changeset |
files
|
| 2009-07-08 |
haftmann |
tuned structure Code internally
|
changeset |
files
|
| 2009-07-08 |
nipkow |
merged
|
changeset |
files
|
| 2009-07-08 |
nipkow |
name fixed
|
changeset |
files
|
| 2009-07-07 |
haftmann |
merged
|
changeset |
files
|
| 2009-07-07 |
haftmann |
merged
|
changeset |
files
|
| 2009-07-07 |
haftmann |
tuned interface of structure Code
|
changeset |
files
|
| 2009-07-07 |
haftmann |
more accurate certificates for constant aliasses
|
changeset |
files
|
| 2009-07-07 |
haftmann |
merged
|
changeset |
files
|
| 2009-07-07 |
haftmann |
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
|
changeset |
files
|
| 2009-07-07 |
wenzelm |
fixed proof (cf. 40501bb2d57c);
|
changeset |
files
|
| 2009-07-07 |
nipkow |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
changeset |
files
|
| 2009-07-07 |
haftmann |
merged
|
changeset |
files
|
| 2009-07-06 |
haftmann |
tuned code
|
changeset |
files
|
| 2009-07-06 |
haftmann |
moved Inductive.myinv to Fun.inv; tuned
|
changeset |
files
|
| 2009-07-06 |
wenzelm |
add_classrel/arity: strip_shyps of stored result;
|
changeset |
files
|
| 2009-07-06 |
wenzelm |
clarified strip_shyps: proper type witnesses for present sorts;
|
changeset |
files
|
| 2009-07-06 |
wenzelm |
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
|
changeset |
files
|
| 2009-07-06 |
wenzelm |
structure Thm: less pervasive names;
|
changeset |
files
|
| 2009-07-06 |
wenzelm |
clarified Thm.of_class/of_sort/class_triv;
|
changeset |
files
|
| 2009-07-06 |
wenzelm |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
changeset |
files
|
| 2009-07-04 |
wenzelm |
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
|
changeset |
files
|
| 2009-07-04 |
wenzelm |
Delayed action.
|
changeset |
files
|
| 2009-07-04 |
wenzelm |
merged
|
changeset |
files
|
| 2009-07-04 |
haftmann |
merged
|
changeset |
files
|
| 2009-07-03 |
haftmann |
nominal.ML is nominal_datatype.ML
|
changeset |
files
|
| 2009-07-03 |
haftmann |
merged
|
changeset |
files
|
| 2009-07-03 |
haftmann |
nominal.ML is nominal_datatype.ML
|
changeset |
files
|
| 2009-07-03 |
haftmann |
cleaned up fundamental iml term functions; nested patterns
|
changeset |
files
|
| 2009-07-03 |
haftmann |
cleaned up fundamental iml term functions
|
changeset |
files
|
| 2009-07-03 |
haftmann |
proper closures -- imperative programming considered harmful...
|
changeset |
files
|
| 2009-07-03 |
haftmann |
avoid useless code equations
|
changeset |
files
|
| 2009-07-03 |
haftmann |
restored subscripts
|
changeset |
files
|
| 2009-07-03 |
haftmann |
lemma foldl_apply_inv
|
changeset |
files
|
| 2009-07-04 |
wenzelm |
is_open: surrogate sequence is High..Low;
|
changeset |
files
|
| 2009-07-03 |
wenzelm |
init/check Isabelle_System;
|
changeset |
files
|
| 2009-07-03 |
wenzelm |
init isabelle home from existing setting or hint via system property;
|
changeset |
files
|
| 2009-07-03 |
wenzelm |
more hgignore;
|
changeset |
files
|
| 2009-07-03 |
wenzelm |
basic setup for Isabelle/JVM application bundle;
|
changeset |
files
|
| 2009-07-03 |
wenzelm |
separate setup for App1;
|
changeset |
files
|
| 2009-07-03 |
wenzelm |
SCALA_HOME: proper line escapes for choosefrom;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
allow reloading of settings within JVM process;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
Isabelle application wrapper for windows.
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
isabelle.home: native jvmpath;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
Generic Isabelle application wrapper.
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
observe SCALA_HOME, if available;
|
changeset |
files
|