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