2012-03-04 blanchet 2012-03-04 ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
2012-03-04 wenzelm 2012-03-04 updates for jedit-4.5.0 (still inactive);
2012-03-04 wenzelm 2012-03-04 more explicit patches;
2012-03-04 wenzelm 2012-03-04 tuned comment;
2012-03-04 wenzelm 2012-03-04 removed obsolete proper_command_at (cf. 03a2dc9e0624);
2012-03-04 wenzelm 2012-03-04 added Command.proper_range (still unused);
2012-03-04 wenzelm 2012-03-04 clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
2012-03-04 wenzelm 2012-03-04 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;
2012-03-04 haftmann 2012-03-04 tuned
2012-03-04 haftmann 2012-03-04 move test targets to test target
2012-03-04 haftmann 2012-03-04 dropped images for importer sessions
2012-03-04 haftmann 2012-03-04 dropped dead code
2012-03-04 haftmann 2012-03-04 more accurate dependencies
2012-03-04 haftmann 2012-03-04 tuned ML
2012-03-04 haftmann 2012-03-04 dropped silly code
2012-03-04 haftmann 2012-03-04 tuned
2012-03-04 haftmann 2012-03-04 dropped dead code
2012-03-04 haftmann 2012-03-04 actually add "the" Importer theory
2012-03-04 haftmann 2012-03-04 avoid internal hol4 name references in generic importer code
2012-03-03 haftmann 2012-03-03 generalized user-visible text
2012-03-03 haftmann 2012-03-03 generalized attribute name
2012-03-03 haftmann 2012-03-03 dropped dead theories
2012-03-03 haftmann 2012-03-03 one unified Importer theory
2012-03-03 haftmann 2012-03-03 added actual dependencies
2012-03-03 haftmann 2012-03-03 import all importer theories in compatibility layer
2012-03-03 wenzelm 2012-03-03 merged;
2012-03-03 haftmann 2012-03-03 dropped obsolete ROOT.ML
2012-03-03 haftmann 2012-03-03 plugged in pre-existing theories appropriately
2012-03-03 haftmann 2012-03-03 switch of target Import-HOL_Light-Imported: not operative at the moment
2012-03-03 haftmann 2012-03-03 turn on quick and dirty in batch mode
2012-03-03 haftmann 2012-03-03 tuned whitespace
2012-03-03 haftmann 2012-03-03 file system structure separating HOL4 and HOL Light concerns
2012-03-03 haftmann 2012-03-03 distribution of compatibility theories
2012-03-03 haftmann 2012-03-03 formal infrastructure for import sessions
2012-03-03 haftmann 2012-03-03 dropped dead code
2012-03-03 haftmann 2012-03-03 tuned whitespace
2012-03-03 haftmann 2012-03-03 spurious set/pred correction
2012-03-03 haftmann 2012-03-03 explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction
2012-03-03 haftmann 2012-03-03 explicit locations for import_theory and setup_theory, for better user interface conformance
2012-03-03 wenzelm 2012-03-03 discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
2012-03-03 wenzelm 2012-03-03 tuned;
2012-03-03 wenzelm 2012-03-03 tuned;
2012-03-03 wenzelm 2012-03-03 tuned;
2012-03-03 wenzelm 2012-03-03 canonical argument order for attribute application;
2012-03-03 wenzelm 2012-03-03 clarified terminology of raw protocol messages;
2012-03-03 wenzelm 2012-03-03 tuned;
2012-03-03 wenzelm 2012-03-03 tuned signature -- emphasize Isabelle_Process Input vs. Output;
2012-03-03 wenzelm 2012-03-03 explicit syslog_limit reduces danger of low-level message flooding; tuned;
2012-03-03 wenzelm 2012-03-03 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;
2012-03-03 wenzelm 2012-03-03 clarified scope of exception handlers;
2012-03-03 wenzelm 2012-03-03 relevant timing as in ML; more PIDE modules;
2012-03-02 haftmann 2012-03-02 more fundamental pred-to-set conversions for range and domain by means of inductive_set
2012-03-02 wenzelm 2012-03-02 merged
2012-03-02 haftmann 2012-03-02 tuned whitespace
2012-03-02 haftmann 2012-03-02 tuned import
2012-03-02 haftmann 2012-03-02 dropped dead code
2012-03-02 wenzelm 2012-03-02 terminate after first exception -- avoid syslog flooding;
2012-03-02 wenzelm 2012-03-02 avoid buffer loading overrun; tuned;
2012-03-02 wenzelm 2012-03-02 merged
2012-03-02 bulwahn 2012-03-02 collecting all axioms in a locale context in quickcheck; adding some verbose output;