export load_thy -- no backpatching;

export subst_alias; moved read_const_exprs to Tools/code_package.ML -- avoids dependency on ThyInfo;

load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;

val theory = ThyInfo.get_theory;

replaced Isar loop variants by generic toplevel_loop;

replaced Isar loop variants by generic toplevel_loop; eliminated obsolete get_interrupt (subsumed by crash handling);

The global Isabelle/Isar state and main read-eval-print loop.

replaced Isar.toplevel by Toplevel.program;

moved global Toplevel state to structure Isar;

made purely value-oriented, moved global state to structure Isar (cf. isar.ML); export toplevel, error_msg (formerly print_exn), transition (formerly apply); moved type isar to structure OuterSyntax; moved crashes to structure Isar;

finish: removed unnecessary Isar.init;

moved structure Isar to isar.ML; added type isar (from toplevel.ML);

Context.set_thread_data: non-critical;

added Isar/isar.ML;

improvements are strict

check validity of class target improvement

print_consts only for external specifications;

fundef_afterqed: removed unused config, added do_print flag; print_consts only for external specifications;

minimal error handling;

replaced ML by ML_val;

avoid control symbols in document (\<^fixed>);

\usepackage[english]{babel} (required for guillemots);

renamed mbind to scomp

removed syntax from monad combinators; renamed mbind to scomp

rudimentary user-syntax for terms

fix spelling

fix spelling

move lemmas from Word/BinBoolList.thy to List.thy

fixed makefiles

added missing file