2012-03-03 haftmann actually add "the" Importer theory
2012-03-03 haftmann avoid internal hol4 name references in generic importer code
2012-03-03 haftmann generalized user-visible text
2012-03-03 haftmann generalized attribute name
2012-03-03 haftmann dropped dead theories
2012-03-03 haftmann one unified Importer theory
2012-03-03 haftmann added actual dependencies
2012-03-03 haftmann import all importer theories in compatibility layer
2012-03-03 wenzelm merged;
2012-03-03 haftmann dropped obsolete ROOT.ML
2012-03-03 haftmann plugged in pre-existing theories appropriately
2012-03-03 haftmann switch of target Import-HOL_Light-Imported: not operative at the moment
2012-03-03 haftmann turn on quick and dirty in batch mode
2012-03-03 haftmann tuned whitespace
2012-03-03 haftmann file system structure separating HOL4 and HOL Light concerns
2012-03-03 haftmann distribution of compatibility theories
2012-03-03 haftmann formal infrastructure for import sessions
2012-03-03 haftmann dropped dead code
2012-03-03 haftmann tuned whitespace
2012-03-03 haftmann spurious set/pred correction
2012-03-03 haftmann explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction
2012-03-03 haftmann explicit locations for import_theory and setup_theory, for better user interface conformance
2012-03-03 wenzelm discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
2012-03-03 wenzelm tuned;
2012-03-03 wenzelm tuned;
2012-03-03 wenzelm tuned;
2012-03-03 wenzelm canonical argument order for attribute application;
2012-03-03 wenzelm clarified terminology of raw protocol messages;
2012-03-03 wenzelm tuned;
2012-03-03 wenzelm tuned signature -- emphasize Isabelle_Process Input vs. Output;
2012-03-03 wenzelm explicit syslog_limit reduces danger of low-level message flooding;
2012-03-03 wenzelm retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
2012-03-03 wenzelm clarified scope of exception handlers;
2012-03-03 wenzelm relevant timing as in ML;
2012-03-02 haftmann more fundamental pred-to-set conversions for range and domain by means of inductive_set
2012-03-02 wenzelm merged
2012-03-02 haftmann tuned whitespace
2012-03-02 haftmann tuned import
2012-03-02 haftmann dropped dead code
2012-03-02 wenzelm terminate after first exception -- avoid syslog flooding;
2012-03-02 wenzelm avoid buffer loading overrun;
2012-03-02 wenzelm merged
2012-03-02 bulwahn collecting all axioms in a locale context in quickcheck;
2012-03-02 bulwahn choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
2012-03-02 bulwahn removing finiteness goals
2012-03-02 bulwahn adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
2012-03-01 wenzelm Symbol.encode header edits;
2012-03-01 wenzelm merged
2012-03-01 haftmann tuned whitespace
2012-03-01 haftmann more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2012-03-01 paulson Removal of obsolete ML bindings
2012-03-01 wenzelm more robust locking;
2012-03-01 wenzelm proper update_header;
2012-03-01 wenzelm refined node_header -- more direct buffer access (again);
2012-03-01 wenzelm merged
2012-03-01 blanchet improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
2012-03-01 blanchet fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction
2012-03-01 blanchet more robust set element extractor
2012-03-01 boehmes fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
2012-03-01 wenzelm tuned proofs;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip