2010-01-05 wenzelm 2010-01-05 tuned message;
2010-01-05 wenzelm 2010-01-05 tuned;
2010-01-05 wenzelm 2010-01-05 added Promise.fulfill_result;
2010-01-05 wenzelm 2010-01-05 slightly shorter tail (again) -- theory loader produces less warning spam (cf. 2524c1bbd087);
2010-01-05 wenzelm 2010-01-05 kill failed theories in reverse order -- avoids cascaded warnings;
2010-01-04 wenzelm 2010-01-04 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 wenzelm 2010-01-04 Standard_System.raw_exec; more robust root.mkdirs;
2010-01-04 wenzelm 2010-01-04 removed function "isabelle-process", keeping "isabelle" only -- functions within the process environment might get passed through a genuine /bin/sh, which does not allow non-identifiers here;
2010-01-04 wenzelm 2010-01-04 added Cygwin "make" package;
2010-01-04 wenzelm 2010-01-04 discontinued old ISABELLE and ISATOOL environment settings;
2010-01-04 wenzelm 2010-01-04 shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;
2010-01-04 wenzelm 2010-01-04 removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
2010-01-04 wenzelm 2010-01-04 merged
2010-01-04 haftmann 2010-01-04 code cache only persists on equal theories
2010-01-04 haftmann 2010-01-04 moved name duplicates to end of theory; reduced warning noise
2010-01-04 haftmann 2010-01-04 merged
2010-01-04 haftmann 2010-01-04 modernized
2010-01-04 haftmann 2010-01-04 added applify combinator
2010-01-04 haftmann 2010-01-04 dropped redundant name declarations
2010-01-04 haftmann 2010-01-04 dropped copy operation for legacy TheoryDataFun
2010-01-04 haftmann 2010-01-04 code cache without copy; tuned
2010-01-04 wenzelm 2010-01-04 report keywords as singleton messages, control message kind via print mode;
2010-01-04 wenzelm 2010-01-04 explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
2010-01-04 wenzelm 2010-01-04 omit useless (?) scaladoc;
2010-01-04 wenzelm 2010-01-04 added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
2010-01-04 wenzelm 2010-01-04 after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;
2010-01-04 wenzelm 2010-01-04 discontinued special HOL_USEDIR_OPTIONS;
2010-01-03 wenzelm 2010-01-03 updated stats;
2010-01-03 wenzelm 2010-01-03 made SML/NJ happy;
2010-01-03 paulson 2010-01-03 merged
2010-01-03 paulson 2010-01-03 removed legacy asm_lr_simp_tac
2010-01-03 nipkow 2010-01-03 removed more asm_rl's - unfortunately slowdown of 1 min.
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2010-01-02 krauss 2010-01-02 provide simp and induct rules in Function.info
2010-01-02 krauss 2010-01-02 more official data record Function.info
2010-01-02 krauss 2010-01-02 simplified
2010-01-02 krauss 2010-01-02 absorb structures Decompose and Descent into Termination, to simplify further restructuring
2010-01-02 nipkow 2010-01-02 another legacy "asm_lr"
2010-01-02 nipkow 2010-01-02 merged
2010-01-02 nipkow 2010-01-02 removed legacy asm_lr
2010-01-02 wenzelm 2010-01-02 merged
2010-01-01 nipkow 2010-01-01 added lemmas
2010-01-01 nipkow 2010-01-01 added lemma
2010-01-01 nipkow 2010-01-01 removed FIXME
2010-01-02 wenzelm 2010-01-02 tuned error handling;
2010-01-02 wenzelm 2010-01-02 Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;
2010-01-02 wenzelm 2010-01-02 Download URLs -- with progress monitor.
2010-01-01 wenzelm 2010-01-01 Future values -- Scala version.
2009-12-31 wenzelm 2009-12-31 added simple dialogs;
2009-12-31 wenzelm 2009-12-31 added is_ready;
2009-12-30 wenzelm 2009-12-30 simplified init message -- removed redundant session property;
2009-12-30 wenzelm 2009-12-30 removed obsolete version check -- sanity delegated to Isabelle_System; tuned;
2009-12-30 wenzelm 2009-12-30 eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id; eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;
2009-12-30 wenzelm 2009-12-30 tuned signature;
2009-12-30 wenzelm 2009-12-30 less ambitious isatest for SML/NJ;
2009-12-30 krauss 2009-12-30 killed a few warnings
2009-12-30 krauss 2009-12-30 more regular axiom of infinity, with no (indirect) reference to overloaded constants
2009-12-29 wenzelm 2009-12-29 back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
2009-12-29 wenzelm 2009-12-29 removed slightly odd Isar_Document.init; simplified begin_document: associate empty command/state with no_id, which is implicit start; replaced make_id by create_id (cf. Scala version); eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var; tuned;
2009-12-29 wenzelm 2009-12-29 explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;