add_path / reset_path;

tuned;

ThmDatabase.ml_store_thm;

usedir -r;

Session.init;

Theory loader database: theory and file dependencies, theory values and user data.

tidied;

Session management -- maintain state of logic images.

get_lexicon; parse_thy: eliminated name, get exploded text; simplified header handling;

tokenize: get exploded args;

delete_tmpfiles (from thy_read.ML); get_lexicon; load_thy;

added reset_path; added ml_path; loader primitives: ml and time arg;

open BasicThmDatabase; Present.thm;

Theory presentation (fake implementation);

moved to Pure/context.ML;

nuked;

moved to General/use.ML;

removed load; detect old vs. new header; provide deps_thy, load_thy primitives for ThyLoad;

ThyInfo.begin_theory;

oops, update_thy;

removed load; added update_thy;

removed load; proper use (ThyInfo.load_file); added use_thy, update_thy;

comment;

removed load;

proper setup of preloaded theories (ThyInfo.register_theory);

renamed sig to PRIVATE_SIGN;

added thm, thms, Open_locale, Close_locale, Print_scope;

added Goal(w) and Export (from context.ML);

added is_draft; renamed sig to PRIVATE_THEORY;

enabled sig;

tuned msg;

Global theory context (used to be in Thy/context.ML);

moved several files;

more abstract implementation;

use Path.T; added 'cd', 'rm', 'use';

of_file: Path.T, Position.T;

added use.ML;

added Use;

tuned;

tidied; added thy_load.ML

tidied, with left_inverse & right_inverse as default simprules

auto update

inj

documented typecheck_tac, etc

standard spelling: type-checking

inj is now a translation of inj_on

standard spelling: type-checking

a bit of tidying

Theory loader primitives.

corrected output of symbols for several (probably not all) relevant functions moved print_mode to ROOT.ML

renamed space2 to spacespace prepared switch for escaped output of symbols (used for ProofGeneral in connection with the x-symbol package)

corrected output of symbols for several (probably not all) relevant functions

moved print_mode to ROOT.ML

expandshort

expandshort

tidied

tidied

constdefs

tidying

arith_tac for min/max

*** empty log message ***

ZF typechecking

automatic insertion of datatype intr rules into claset

new typechecking solver for the simplifier

tuned;

Fixed a bug in lin.arith.

tuned;

tuned;

isabelle.in.tum.de;

http://isabelle.in.tum.de/dist/;

renamed variables for clarity

changed Minho mirror;

tidied freeness reasoning

freeness reasoning: T.free_iffs

tuned;

removal of the (thm list) argument of mk_cases

tidied; added dest_eq

simplified thanks to the arithmetic prover

updated comments

a simplification by G Bella

structure Graph = Graph;

GraphFun (generic directed graphs); Graph (graphs indexed by strings);

added General/graph.ML: generic direct graphs;

removed empty line (in case of empty begin_state marker) before Level line added printing of subgoals number in Level line

Removed superfluous arith rules from metric_simps

More Arith.

Fixed old bug: selection of constant to be split should depend not just on the name but also on the type.

nat_arith_tac -> arith_tac

More arith refinements.

tuned README;

Pure/General/symbol.ML;

tuned;

deleted the appendices because documentation exists in the HOL and ZF manuals

defined dquotesoff

new manual ZF

the separate FOL and ZF logics manual, with new material on datatypes and inductive definitions

removal of FOL and ZF

minor updates on inductive definitions and datatypes

fixed titles;

tidying of datatype and inductive definitions

files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;

Refined arithmetic.

congruence rules finally use == instead of = and <->

generalized qed_spec_mp code to work for ZF

datatype package improvements

better qed_spec_mp

Simplified interface.

Simplified arithmetic.

'same' method, 'immediate' proof;

tuned msg;

SYNC;

fixed again;