tuned;

PrimitiveDefs.dest/abs_def;

PrimitiveDefs.dest_def; Syntax.standard_read;

Primitive definition forms.

moved support for primitive defs to primitive_defs.ML;

use logic.ML earlier; added primitive_defs.ML;

moved Tools/xml.ML to General/xml.ML (again); added primitive_defs.ML;

PrimitiveDefs.mk_defpair;

be a bit more ressource cautious with multi-threading (-M 20 instead of 99)

fixed syntax

simplified

fixed OCaml bug

*** empty log message ***

renamed keyword "to" to "module_name"

dropped code_axioms

moved appl syntax to PureThy; structure Lexicon: not hidden;

Lexicon.tokenize: do not appen EndToken yet; term: include var, &&;

Lexicon.tokenize: do not appen EndToken yet;

Lexicon.read_indexname/nat/variable;

moved appl syntax to PureThy; SimpleSyntax.read_typ/term/prop;

moved appl syntax to PureThy;

SimpleSyntax.read_prop;

added atbroy9

multi-threading with poly 5.1 test

new attribute [rotated]

tuned comments;

Simple syntax for types and terms --- for bootstrapping Pure.

added Syntax/simple_syntax.ML;

* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;

read_def_terms': restrict scope of disambiguation to individual term;

stream source: non-critical, assuming exclusive ownership;

added type constraints to resolve syntax ambiguities;

made SML/NJ happy;

schedule_tasks: alphabetical order for equivalent tasks;

simultaneous use_thys;

tuned ML bindings;

tuned

dropped code generator setup garbage

syntax fix

corrected code generator module names

new structure for code generator modules

code generator setup improved

adjusted

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;

replaced depth_limit ref by blast_depth_limit configuration option; tuned method setup;

replaced dtK ref by datatype_distinctness_limit configuration option;

moved classical tools from theory IFOL to FOL;

register_thy: more sanity checks;

moved lin_arith stuff to Tools/lin_arith.ML;

proper context for cooper_tac within arith;

tuned LinArith setup;

HOL setup for linear arithmetic -- moved here from arith_data.ML;

added Tools/lin_arith.ML;

tuned;

tuned section "Style"; added section "Thread-safe programming";

undo a change in last commit : give a single name to the inversion lemmas for the same inductive type

Proper interpretation of total orders in lattices.

* Configuration options; * Named collections of theorems;

added configuration options;

removed use/update_thy_only;

find_body goes under meta-quantifier ; tactic generalizes free variables;

Added dependency on langford files in Tools/Qelim

Tuned document

added register_thy (replaces pretend_use_thy_only and really flag); tuned;

ThyInfo.register_thy;

turned fast_arith_split/neq_limit into configuration options;

added global config options;

arith method setup: proper context; turned fast_arith_split/neq_limit into configuration options; tuned signatures; misc cleanup;

arith method setup: proper context;

tuned ML declarations;

simultaneous use_thys; tuned;

dequeue: wait loop while PROTECTED -- avoids race condition;

marked some CRITICAL sections;

updated some of the definitions and proofs

tuned msgs; tuned;

deps: keep thy source text, avoid reloading; schedule: pick the first task with maximal imm_succs;

adapted ThyLoad.deps_thy;

more informative tracing; tuned;

load_thy: avoid reloading of text; tuned;

added of_list_limited (with limit argument); removed of_string_limited;

more informative tracing;

explicit global state argument -- no longer CRITICAL;

added option -T (multithreading trace mode);

critical: improved diagostics; schedule: proper broadcast on wakeup condition;

tuned msg;

NAMED_CRITICAL;

removed obsolete Output.ML_errors/toplevel_errors; moved ML toplevel use commands to pure_setup.ML;

removed obsolete Output.ML_errors/toplevel_errors;

added TOPLEVEL_ERROR (simplified version from output.ML);

removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);

added ML toplevel use commands: Toplevel.program; added install_pp stuff;

removed obsolete install_pp.ML (cf. pure_setup.ML);

replaced program_defs_ref by proper context data (via attribute "program");

renamed Drule.is_dummy_thm to Thm.is_dummy;

added list update;

moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;

Named collections of theorems in canonical order.

added Tools/named_thms.ML;

renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; tuned;

avoid ill-defined Simp_tac;

marked some CRITICAL sections;

simplified ResAtpset via NamedThmsFun;

metis_tac: proper context (ProofContext.init it *not* sufficient); simplified method setup;

proper simproc_setup for "neq", "let_simp"; removed dead code;

renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;

replaced make_imp by rev_mp;

proper simproc_setup for "list_neq";

removed obsolete Tools/res_atpset.ML;

simplified ResAtpset via NamedThmsFun; proper simproc_setup for "neq", "let_simp";

simplified "eval" setup via NamedThmsFun;

tuned;

* Isar: command 'declaration'; * Isar: proper interfaces for simplification procedures; * Isar: an extra pair of brackets around attribute declarations abbreviates a theorem reference involving an internal dummy fact;

type Morphism.declaration;

attribute "option": proper naming within the theory

removed dead code;

declaration: proper naming within the theory;

use config_option.ML after sign.ML;

commands 'declare', 'declaration';

added :|-- (dependent projection); tuned;

added attribute "simproc"; marked some CRITICAL sections; tuned;

setmp: NAMED_CRITICAL;