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.;
2009-12-28 wenzelm 2009-12-28 tuned;
2009-12-28 wenzelm 2009-12-28 crude Cygwin.setup;
2009-12-28 wenzelm 2009-12-28 ignore undefined environment;
2009-12-28 wenzelm 2009-12-28 separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
2009-12-28 wenzelm 2009-12-28 tuned;
2009-12-28 wenzelm 2009-12-28 system shutdown hook: strict kill;
2009-12-28 wenzelm 2009-12-28 moved Library.decode_permissive_utf8 to Isabelle_System; moved Library.with_tmp_file to Isabelle_System; added Isabelle_System.read_file/write_file; added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C);
2009-12-28 wenzelm 2009-12-28 pid without newline -- required for Scala version of system_out;
2009-12-28 wenzelm 2009-12-28 higher-order treatment of temporary files;
2009-12-28 wenzelm 2009-12-28 isabelle_tool: apply platform_path only once; tuned;
2009-12-28 wenzelm 2009-12-28 slightly more paranoid cleanup of process (cf. http://kylecartmell.com/?p=9 "Five Common java.lang.Process Pitfalls");
2009-12-28 wenzelm 2009-12-28 some sanity checks for symbol interpretation;
2009-12-27 wenzelm 2009-12-27 allow UTF-8 in theory and file names;
2009-12-27 wenzelm 2009-12-27 factored-out Library.decode_permissive_utf8;