simplified and tidied the proofs

check_mlhome_file;

isatool fixgoal;

isatool fixgoal;

def_sort;

renamed Thm(s) back to thm(s);

export mk_triple1/2;

added read_def_axm;

added fix_mixfix;

fixed comment

tidying

New example Kerberos_BAN by G Bella

fixed comment;

tuned \s pattern;

isatool fixgoal;

removed Thy; the_context made public;

replaced warning by error_msg;

new toplevel commands `Goal' and `Goalw'; isatool fixgoal;

renamed thm(s) to Thm(s);

replace goal(w) commands by implicit versions Goal(w);

Goal and Goalw

goal -> Goal

Changed and changed back.

Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.

added General/history.ML;

Histories of values, with undo and redo;

use_text replaces use_strings;

handle_error: capture error msgs, even if no exception raised;

removed use_text;

added use_text;

Context.add_session;

changed (| |) syntax to (: :);

changed {: :} syntax to (| |);

tuned exports; added Thy;

removed rel.ML

ancient relic

Context.the_context;

get_context renamed to the_context; added get_context, set_context;

tuned transaction;

tuned comments;

adapted to TheoryDataFun interface;

moved attributes theory data to Isar/isar_thy.ML;

moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;

added exnMessage;

added General;

added of_file;

General tools.

moved table.ML, object.ML, seq.ML, name_space.ML to General;

moved object.ML to General/object.ML;

moved table.ML to General/table.ML;

moved seq.ML to General/seq.ML;

moved position.ML, path.ML, file.ML to General;

moved name_space.ML to General/name_space.ML;

moved Thy/path.ML to General/path.ML;

moved Thy/position.ML to General/position.ML;

moved Thy/file.ML to General/file.ML;

new type-safe user interface for theory data;

nonterminals prog;

adapted to new theory data interface;

use type-safe theory data interface;