| 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
|
| 2009-07-02 |
wenzelm |
merged
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
|
changeset |
files
|
| 2009-07-02 |
haftmann |
merged
|
changeset |
files
|
| 2009-07-02 |
haftmann |
instance arities can be simultaneous
|
changeset |
files
|
| 2009-07-02 |
haftmann |
updated generated files
|
changeset |
files
|
| 2009-07-02 |
haftmann |
more friendly wrt. PGs interpretation of compound *); added dedicated section on value and quickcheck
|
changeset |
files
|
| 2009-07-02 |
paulson |
merged
|
changeset |
files
|
| 2009-07-02 |
paulson |
Deleted some debugging code
|
changeset |
files
|
| 2009-07-01 |
paulson |
merged
|
changeset |
files
|
| 2009-06-24 |
paulson |
merged
|
changeset |
files
|
| 2009-06-23 |
paulson |
merged
|
changeset |
files
|
| 2009-06-18 |
paulson |
Removed unnecessary conditions concerning nonzero divisors
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
strip_shyps: remove top sort, which is logically insignificant;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
added pro-forma proof constructor Inclass;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
misc tuning;
|
changeset |
files
|
| 2009-07-02 |
wenzelm |
fixed document (DERIV_intros);
|
changeset |
files
|
| 2009-06-30 |
wenzelm |
more detailed timing message;
|
changeset |
files
|
| 2009-06-30 |
wenzelm |
default to maximum max_threads;
|
changeset |
files
|
| 2009-06-30 |
wenzelm |
merged
|
changeset |
files
|
| 2009-06-30 |
wenzelm |
fixed ISABELLE_HOME_USER;
|
changeset |
files
|
| 2009-06-30 |
haftmann |
merged
|
changeset |
files
|
| 2009-06-30 |
haftmann |
adaptated to changes in term representation
|
changeset |
files
|
| 2009-06-30 |
haftmann |
improved treatment of case patterns
|
changeset |
files
|
| 2009-06-30 |
haftmann |
merged
|
changeset |
files
|
| 2009-06-30 |
haftmann |
an intermediate step towards a refined translation of cases
|
changeset |
files
|
| 2009-06-30 |
haftmann |
all variable names are optional
|
changeset |
files
|
| 2009-06-30 |
haftmann |
variable names in abstractions are optional
|
changeset |
files
|
| 2009-06-30 |
haftmann |
restored
|
changeset |
files
|
| 2009-06-30 |
wenzelm |
added isatest for x86_64-darwin;
|
changeset |
files
|
| 2009-06-30 |
wenzelm |
merged
|
changeset |
files
|
| 2009-06-30 |
hoelzl |
NEWS updated
|
changeset |
files
|
| 2009-06-30 |
hoelzl |
DERIV_ln is proved in Transcendental and in Ln, use Transcendental to prove Ln.
|
changeset |
files
|
| 2009-06-30 |
hoelzl |
remove DERIV_tac and deriv_tac, neither is used in Isabelle/HOL or the AFP
|
changeset |
files
|
| 2009-06-30 |
hoelzl |
use DERIV_intros
|
changeset |
files
|
| 2009-06-30 |
hoelzl |
Added DERIV_intros
|
changeset |
files
|
| 2009-06-30 |
bulwahn |
commented trancl example; added debug message
|
changeset |
files
|
| 2009-06-30 |
bulwahn |
merged
|
changeset |
files
|
| 2009-06-30 |
bulwahn |
exported is_registered; added debug messages; removed extended parameter compilation in predicate compiler
|
changeset |
files
|
| 2009-06-29 |
bulwahn |
added diagnostic printing; changed proof for parameters; moved code
|
changeset |
files
|
| 2009-06-30 |
haftmann |
merged
|
changeset |
files
|
| 2009-06-30 |
haftmann |
simplified binding concept
|
changeset |
files
|
| 2009-06-30 |
haftmann |
temporary workaround
|
changeset |
files
|
| 2009-06-30 |
haftmann |
tuned
|
changeset |
files
|