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