added int type constraint to accomodate hacked SML/NJ (backported change in generated metis.ML);

preparations for proper type int;

tuned tracing;

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*;

certify: no check_thy here;

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;

moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;

added dependency on Tools/Metis/metis.ML;

updated;

replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;

reset Logic.auto_rename;

added int type constraints to accomodate hacked SML/NJ;

added int type constraints to accomodate hacked SML/NJ;

added int type constraints to accomodate hacked SML/NJ;

made mk_int/dest_int pervasive;

Experimental removal of assumptions of the form x : UNIV and the like after interpretation.

Repaired term_of_char.

- 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.

tuned;

converted Meson tests to proper theory;

turned simp_depth_limit into configuration option; tuned register_config;

added name_of;

turned simp_depth_limit into configuration option;

tuned ML bindings (for multithreading); updated timings;

tuned ML bindings (for multithreading);

fix looping when applied to standard subgoals

updated;

tracing: level;

multithreading trace: int;

added toplevel print command;

tuned;

renamed 'print_options' to 'print_configs';