2007-12-11 ago haftmann error handling for pathological cases
2007-12-11 ago haftmann dropped induction rule
2007-12-11 ago haftmann dropped Class.prep_spec
2007-12-11 ago haftmann moved lemma odd_pos to theory Parity
2007-12-11 ago haftmann joined StarClasses theory with StarDef
2007-12-11 ago haftmann joined EvenOdd theory with Parity
2007-12-11 ago haftmann tuned
2007-12-10 ago haftmann added simple primitive note
2007-12-10 ago haftmann moved instance parameter management from class.ML to axclass.ML
2007-12-10 ago haftmann tuned header
2007-12-10 ago haftmann switched import from Main to List
2007-12-10 ago haftmann switched import from Main to PreList
2007-12-10 ago haftmann explicit import of theory ATP_Linkup
2007-12-10 ago haftmann explicit import of theory Main
2007-12-10 ago haftmann swtiched ATP_Linkup and PreList in theory hierarchy
2007-12-09 ago wenzelm ML_OPTIONS="-H 1500" -- potentially works around GC core dump;
2007-12-09 ago krauss added Id, some cleanup
2007-12-08 ago wenzelm tuned message;
2007-12-08 ago wenzelm renamed IsabelleResult to IsabelleProcess.Result;
2007-12-08 ago wenzelm Isabelle process wrapper for JVM platform (tentative implementation in
2007-12-08 ago wenzelm tuned messages;
2007-12-08 ago wenzelm Isar loop: recover after toplevel crashes;
2007-12-08 ago wenzelm secure_main: enforces terminator, to gain robustness;
2007-12-08 ago wenzelm text_of: make double sure that result is well-formed, to avoid recurrent failures;
2007-12-08 ago wenzelm ML_OPTIONS="-H 1000" -- potentially works around GC core dump;
2007-12-07 ago wenzelm added off-line parse;
2007-12-07 ago wenzelm (alt)string: allow explicit character codes (as in ML);
2007-12-07 ago wenzelm added nested 'Isabelle.command';
2007-12-07 ago wenzelm updated;
2007-12-07 ago wenzelm special_end: replaced Z by dot;
2007-12-07 ago wenzelm output_prompt: CRITICAL;
2007-12-07 ago haftmann declaration of instance parameter names
2007-12-07 ago haftmann exported declare_names
2007-12-07 ago haftmann new primrec
2007-12-07 ago haftmann instantiation target rather than legacy instance
2007-12-07 ago haftmann proper treatment of code theorems for primrec
2007-12-07 ago haftmann dropped Instance.instantiate
2007-12-07 ago krauss Adding "ex/Induction_Scheme.thy" to tests
2007-12-07 ago krauss experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
2007-12-07 ago haftmann tuned further
2007-12-06 ago wenzelm renamed ML_PID to PID;
2007-12-06 ago nipkow R&F: added sgn lemma
2007-12-06 ago haftmann temporary code generator work arounds
2007-12-06 ago haftmann fixed slip
2007-12-06 ago haftmann -authentic primrec
2007-12-06 ago haftmann dropped legacy bindings
2007-12-06 ago haftmann authentic primrec
2007-12-06 ago haftmann dropped void space
2007-12-06 ago haftmann added new primrec package
2007-12-06 ago krauss load sum_tree.ML
2007-12-06 ago krauss factored out handling of sum types again
2007-12-06 ago wenzelm added test_markup;
2007-12-06 ago wenzelm moved basic test_markup to isabelle_process.ML;
2007-12-06 ago wenzelm added channels;
2007-12-06 ago wenzelm replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;
2007-12-06 ago wenzelm check persistent sessions;
2007-12-05 ago wenzelm tuned signature;
2007-12-05 ago wenzelm made SML/NJ happy;
2007-12-05 ago wenzelm removed -e flag from most sessions;
2007-12-05 ago obua instance int,real :: lordered_ring