2007-08-08 wenzelm 2007-08-08 thread-safeness: when creating certified items, perform Theory.check_thy *last*; tuned datatype proof;
2007-08-08 paulson 2007-08-08 Code to undo the function ascii_of
2007-08-08 paulson 2007-08-08 Fixing the code to undo the function ascii_of
2007-08-08 paulson 2007-08-08 metis
2007-08-07 wenzelm 2007-08-07 tuned ML setup;
2007-08-07 wenzelm 2007-08-07 fixed imports from ../../Auth;
2007-08-07 wenzelm 2007-08-07 turned Unify flags into configuration options (global only);
2007-08-07 wenzelm 2007-08-07 usedir: added options -M -T for multithreading;
2007-08-07 wenzelm 2007-08-07 removed 'declare' from tactic emulations;
2007-08-07 wenzelm 2007-08-07 theory loader: removed obsolete update_thy (coincides with use_thy); tuned; tuned comments;
2007-08-07 wenzelm 2007-08-07 theory loader: removed obsolete update_thy (coincides with use_thy);
2007-08-07 wenzelm 2007-08-07 theory loader: added use_thys, removed obsolete update_thy;
2007-08-07 wenzelm 2007-08-07 theory loader: added use_thys, removed obsolete update_thy; various global ML references of Pure and HOL have been turned into configuration options;
2007-08-07 krauss 2007-08-07 Issue a warning, when "function" encounters variables occuring in function position, as in "f (g x) = ..." where g is a variable.
2007-08-07 krauss 2007-08-07 more error handling
2007-08-07 wenzelm 2007-08-07 added more instances;
2007-08-07 krauss 2007-08-07 simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"
2007-08-07 haftmann 2007-08-07 split off Option theory
2007-08-07 haftmann 2007-08-07 new nbe implementation
2007-08-07 haftmann 2007-08-07 more robust simproces
2007-08-07 haftmann 2007-08-07 tuned
2007-08-07 haftmann 2007-08-07 simplified proofs
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-08-07 haftmann 2007-08-07 changed import order
2007-08-06 wenzelm 2007-08-06 added more instances;
2007-08-06 wenzelm 2007-08-06 ML-Systems/overloading_smlnj.ML;
2007-08-06 wenzelm 2007-08-06 Overloading in SML/NJ.
2007-08-06 berghofe 2007-08-06 Added renaming function to prevent correctness proof for realizer of induction rule to fail because of name clashes between parameters and predicate variables.
2007-08-06 berghofe 2007-08-06 No document for Pretty_Int theory.
2007-08-06 haftmann 2007-08-06 nbe improved
2007-08-06 haftmann 2007-08-06 removed
2007-08-03 wenzelm 2007-08-03 simultaneous use_thys;
2007-08-03 wenzelm 2007-08-03 reactivated Nominal/Examples/Class.thy;
2007-08-03 wenzelm 2007-08-03 replaced outdated flag by update_time (multithreading-safe presentation order);
2007-08-03 wenzelm 2007-08-03 sort indexes according to symbolic update_time (multithreading-safe);
2007-08-03 wenzelm 2007-08-03 use separate trace flag instead of Output.debug;
2007-08-03 wenzelm 2007-08-03 named some CRITICAL sections;
2007-08-03 wenzelm 2007-08-03 misc cleanup of ML bindings (for multihreading);
2007-08-03 wenzelm 2007-08-03 added int type constraint to accomodate hacked SML/NJ (backported change in generated metis.ML);
2007-08-03 wenzelm 2007-08-03 preparations for proper type int;
2007-08-03 wenzelm 2007-08-03 tuned tracing;
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref; thread-safeness: when creating certified items, perform Theory.check_thy *last*;
2007-08-03 wenzelm 2007-08-03 certify: no check_thy here;
2007-08-03 wenzelm 2007-08-03 improved check_thy: produce a checked theory_ref (thread-safe version); removed obsolete self_ref (cf. check_thy); thread-safeness: when creating certified items, perform Theory.check_thy *last*; eq_thy: no check here; marked some critical sections;
2007-08-03 wenzelm 2007-08-03 moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
2007-08-03 wenzelm 2007-08-03 added dependency on Tools/Metis/metis.ML;
2007-08-03 wenzelm 2007-08-03 updated;
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-08-02 wenzelm 2007-08-02 reset Logic.auto_rename;
2007-08-02 wenzelm 2007-08-02 added int type constraints to accomodate hacked SML/NJ;
2007-08-02 wenzelm 2007-08-02 added int type constraints to accomodate hacked SML/NJ;
2007-08-02 wenzelm 2007-08-02 added int type constraints to accomodate hacked SML/NJ;
2007-08-02 wenzelm 2007-08-02 made mk_int/dest_int pervasive;
2007-08-02 ballarin 2007-08-02 Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
2007-08-02 berghofe 2007-08-02 Repaired term_of_char.
2007-08-02 berghofe 2007-08-02 - Added cycle test to function mk_ind_def to avoid non-termination of code generator. - Functions generated from inductive predicates having neither parameters nor input arguments now take a unit element as an argument, otherwise the generated code would be ill-formed.
2007-08-02 wenzelm 2007-08-02 tuned;
2007-08-02 wenzelm 2007-08-02 converted Meson tests to proper theory;
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option; tuned register_config;
2007-08-02 wenzelm 2007-08-02 added name_of;