new structure for code generator modules

ClassPackage renamed to Class

updated

simultaneous use_thys;

removal of some refs

(un)interruptible: pass-through original thread attributes;

tuned; added jEdit mode spec;

HOL_USEDIR_OPTIONS: default to -M 1 (more robust);

added jEdit mode spec; tuned comments;

* Experimental support for multithreading, using Poly/ML 5.1;

schedule: misc cleanup, more precise task model;

schedule: more precise task model; improved error handling: first failure causes interrupt of all threads; misc cleanup;

schedule: more precise task model; removed obsolete structure Task;

fixed DESCRIPTION: single line; proper quoting of shell variables;

updated;

adapted ThyLoad.check_thy;

dropped

explizit checking for pattern discipline

proper handling of empty datatypes

improved class target: now considers class intro rules

new access interface in defs.ML

adaptions for code generation

proper implementation of rational numbers

localized of_nat

tuned

re-eliminated Option.thy

updated

PGIP change: thyname is optional in opentheory, markup even in case of header parse failure

Typo in comment

discontinued attached ML files; end_theory: fail on unresolved dependencies;

simplified ThyLoad.deps_thy etc.: discontinued attached ML files;

load_thy: try_ml_file unconditionally;

* Theory loader: old-style ML proof scripts are considered a legacy feature;

check_deps: really do reload the master text if required; load_thy: more robust check of corrupted deps; require_thy: outdate_thy if required; tuned;

Useful abbreviation of isatool commands used by Eclipse

thread-safeness: when creating certified items, perform Theory.check_thy *last*; tuned datatype proof;

Code to undo the function ascii_of

Fixing the code to undo the function ascii_of

metis

tuned ML setup;

fixed imports from ../../Auth;

turned Unify flags into configuration options (global only);

usedir: added options -M -T for multithreading;

removed 'declare' from tactic emulations;

theory loader: removed obsolete update_thy (coincides with use_thy); tuned; tuned comments;

theory loader: removed obsolete update_thy (coincides with use_thy);

theory loader: added use_thys, removed obsolete update_thy;

theory loader: added use_thys, removed obsolete update_thy; various global ML references of Pure and HOL have been turned into configuration options;

Issue a warning, when "function" encounters variables occuring in function position, as in "f (g x) = ..." where g is a variable.

more error handling

added more instances;

simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"

split off Option theory

new nbe implementation

more robust simproces

tuned

simplified proofs

split off theory Option for benefit of code generator

changed import order

added more instances;

ML-Systems/overloading_smlnj.ML;

Overloading in SML/NJ.

Added renaming function to prevent correctness proof for realizer of induction rule to fail because of name clashes between parameters and predicate variables.

No document for Pretty_Int theory.

nbe improved

removed

simultaneous use_thys;

reactivated Nominal/Examples/Class.thy;

replaced outdated flag by update_time (multithreading-safe presentation order);

sort indexes according to symbolic update_time (multithreading-safe);

use separate trace flag instead of Output.debug;

named some CRITICAL sections;

misc cleanup of ML bindings (for multihreading);

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

renamed config_option.ML to config.ML; moved attrib setup to attrib.ML;

renamed config_option.ML to config.ML;

simplified internal Config interface;

updated;

tuned config options: eliminated separate attribute "option";

oops -- fixed syntax;

"running": PROTECTED wakeup; "cont": actually invoke wakeup!!

proper path specifications;

simultaneous use_thys;

setmp_noncritical print_mode;

simultaneous use_thys;

removed obsolete HOL/Real/ROOT.ML;

no_document: setmp_noncritical;

with_charset: setmp_noncritical;

added max-threads preference;