add_path;

Hyperreal made part of Real;

Session.use_dir: check parent;

*** empty log message ***

more robust handling of theory context; header-only theory files;

improved theory, context, update_context;

improved 'theory'; context / update_context autoload;

improved msg;

use_thy, update_thy: Context.save;

tuned;

time_use made pervasive; load_file: time option; tuned;

use_dir: check parent, more robust exit;

more robust RC;

setmp: theory option; save;

Session.finish (); use;

tidied Schroeder-Bernstein proof

new surj rules

obsolete;

tuned;

include full paths in file info; include (optional) ML file in master info;

Symbol.use;

Symbol.use (eliminated Use.exit_use);

leave theory context after load_thy;

File.pwd, File.cd;

fixed file_info;

use, cd;

added 'use';

fail_safe close; added sys_unpack hook; added pwd; removed join_info;

check_elem: allow ~, except for '~' and '~~';

removed use.ML;

removed General/use.ML;

made SML/NJ happy;

check_thy: include ML stamp;

added join_info;

tidied load path handling;

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