chmod u+rw on all files;

tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);

deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy); begin_theory: quiet_update_thys in interactive mode, removed no weak_use_thy in batch mode; misc tuning;

tuned;

dropped Nat legacy bindings

check_file: fall back on Path.current;

tuned;

* Theory loader: be more serious about observing the static theory header specifications; * Theory loader: optional support for content-based file identification;

added ISABELLE_FILE_IDENT;

simplified ThyLoad interfaces: only one additional directory; require_thy: cumulative appending of directory prefix; tuned;

simplified ThyLoad interfaces: only one additional directory; recovered usualy load_path semantics: only basic names are looked up;

simplified ThyLoad interfaces: only one additional directory;

new functions cut_matrix', etc.

dropped Nat.ML legacy bindings

moved class ord from Orderings.thy to HOL.thy

dropped Nat.ML legacy bindings

split class abs from class minus

simplified HOL bootstrap

tuned;

ThyHeader.read: Source.of_string_limited;

added of_string_limited (more efficient for partial scans);

added rep_ident;

added pprint for Path.T, File.ident;

tuned signature; load_path: always used, even for partially qualified path names; check_file: precise (no adding of extensions!); misc cleanup;

removed obsolete use/update_thy_only; removed unused quiet_update_thy, get_succs; renamed get_preds to get_parents; deps: replaced File.info by File.ident (no comparison of paths!); check_deps: reload (partially qualified) parents for unfinished theory, no reference of previously loaded master paths! require_thy: attempt at purely static path lookup, less permissive; misc cleanup;

adapted ThyLoad.check_file etc.; tuned signature;

adapted ThyLoad.deps_thy

adapted ThyHeader.read;

adapted ThyLoad.check_file;

moved deps_thy to ThyLoad (independent of outer syntax); tuned load_thy;

removed obsolete use/update_thy_only;

use thy_header.ML earlier;

tuned signature;

tuned;

replaced info by ident (for full identification, potentially content-based); ident: invoke external lib/scripts/fileident, depending on ISABELLE_FILE_IDENT;

added undefined: 'a -> 'b;

support for SML builtin ints

adapted to new code generator framework

code lemma for contents

code lemma for of_int

tuned

uniform naming conventions for CG theories

added lemmas by Brian Huffman

moved set Nats to Nat.thy

added of_int_of_nat

updated

strong_ind_simproc now only rewrites arguments of inductive predicates.

updated

Refer to major premise of induction rule via "thm_style prem1".

Added named_thms antiquotation.

Replaced "hand-made" files by generated files in Inductive/document.

LaTeX code is now generated directly from theory files.

LaTeX code is now generated directly from Even and Advanced theories.

LaTeX code is now generated directly from theory file.

DEEPEN: Use priority message channel for interim messages (not warnings).

Direct priority and tracing channels properly.

tidying using metis

fileident --- produce file identification based;

added ISABELLE_FILE_IDENT (command line for source file identification);

adapted TextIO.inputLine;