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;

tuned comment;

avoid redundant variables in patterns (which made Alice vomit);

Full sort information by default. Race condition on successful proofs fixed.

Added hypotheses.

Added clause for hypotheses to proof_of_xml function.

use /usr/proj/polyml/polyml-5.1-test, which might be more stable;

reverted fun->recdef, since there are problems with induction rule

Pure theory setup.

Generic print mode.

moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);

simplified loading of ML files -- no static forward references;

moved print_translations from Pure.thy to Syntax/syn_trans.ML;

added General/print_mode.ML, pure_setup.ML;

tuned specifications;

use function package

more proofs

some interface cleanup

added lemma binding: accpI = accp.accI

updated

tidied using sledgehammer

tidied

tidied using sledgehammer

tidied using sledgehammer

clarified structure names

added function for case certificates

dropped outer ROOT structure for generated code

tuned

fixed SML/NJ int problem

updated

tuned;

updated

updated;

tuned signature; misc cleanup / simplification;

sys_error;

simplified using Markup.get_int; renamed PgipParser to OldPgipParser;

added skeleton for print_mode setup; removed unused stuff;

tuned spacing;

renamed PgipParser to OldPgipParser;

Parsing theory sources without execution (via keyword classification).

exported command_keyword; tuned;

command 'declare': proper thy_decl;

added get_string, get_int; tuned;

added ProofGeneral/pgip_parser.ML;

tuned error faces;

tries to solve goal via TrueI

tuned markup;

replaced OuterLex.name_of by more sophisticated OuterLex.text_of;

Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols); replaced OuterLex.name_of by more sophisticated OuterLex.text_of; tuned;

Buffer.markup;

removed ident, space; added antiq; tuned;

added markup operation;

Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);

Added entry for new inductive definition package.

Proof terms for meta-conjunctions are now normalized before splitting up the conjunctions.

Added function norm_proof for normalizing the proof term corresponding to a theorem.

Added function rew_proof (for pre-normalizing proofs).

Function unify_consts moved from OldInductivePackage to PrimrecPackage.

Adapted to new inductive definition package.

Renamed accessible part for predicates to accp.

renamed inductive2 to inductive.

Renamed inductive2 to inductive.

Hide member constant.