non-transparent logo;

fixed dots;

hierachically structured name spaces;

Changed logo.

Added command for copying new logo.

fixed dots;

fixed dots;

fixed fixed dots;

fixed dots;

fixed dots;

tuned;

fixed dots;

fixed dots;

fixed dots;

BAD_space_explode;

tuned; more accesses to long name;

fixed space_explode, old one retained as BAD_space_explode; added split_lines;

scan_longid moved to Syntax/lexicon.ML;

constify: qualified is const;

added longid syntax;

added longid;

decode: qualified is always const;

tuned;

\n at end;

ensure that dots in formulas are followed by non-idents;

*** empty log message ***

no longer handles consts "" -- use syntax instead; pretty printer: changed order of mixfix annotation preference (again!);

removed open;

fixed infix syntax;

added TLA stuff;

fixed oracle;

removed declIffOracle;

changed preference order of prtab entries;

fixed infix syntax;

improved oracles: named, many per theory; name spaces: thmK, oracleK;

improved oracle: name; optional begin after thy header, with warning;

fixed get_axiom, invoke_oracle; improved Oracle deriv;

print_theory: added oracles;

tuned exports; tuned add_space; tuned print_sg; fixed "op ==>" syntax;

fixed axiom names;

symbols syntax;

A formalization of TLA in HOL -- by Stephan Merz;

improved types of add_XXX funs (xtyp etc.);

improved types of add_XXX funs (xtyp etc.); tuned comments; tuned msgs; improved merge: no longer raises ERROR, but TERM;

tuned decode;

tuned internal mapping table; improved merge: 2nd overrides 1st;

tuned;

tuned warning msg;

tuned;

The Isabelle Logo;

fixed 'begin';

optional begin keyword;

"->" made syntax;

eliminated raise_term;

eliminated raise_term, raise_typ;

add_arities_i;

TODO: handle internal / external names;

now supports qualified names (intern vs. extern) !!! added long_names: bool ref (initially false); new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i; rep_sg: added path, spaces; added pretty_sort (uses proper syntax); improved print_sg; eliminated raise_term, raise_typ;

eliminated raise_term, raise_typ; tuned get_sort, decode_types, infer_types to accomodate qualified names;

tuned read_cterms;

eliminated raise_term, raise_typ; new internal forms: add_inst_subclass_i, add_inst_arity_i;

new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i added add_path, add_space; eliminated raise_term;

tuned;

now uses new Sign.pretty_sort;

eliminated raise_term, raise_typ;

now uses Syntax.simple_str_of_sort;

added simple_str_of_sort;

eliminated raise_term;

added 'path' section; root path at end;

added pretty_sort; tuned read_typ; tuned pretty_term; removed string_of_term, string_of_typ;

fixed raw_term_sorts (again!); eliminated raise_ast;

eliminated raise_ast, raise_term, raise_typ;

added sort_to_ast; eliminated raise_ast;

eliminated raise_ast;

RAW target;

syntactic constants;

Routine tidying up

fully qualified names: Theory.add_XXX;

fully qualified name: Theory.set_oracle;

exported separator;

fully qualified names: Theory.add_XXX;

moved theory stuff (add_defs etc.) here from drule.ML; only BasicTheory opened;

moved theory stuff (add_defs etc.) to theory.ML;

fully qualified name: Theory.merge_thy_list;

fully qualified names: Theory.add_XXX;

added name_space.ML;

added split_last;

Hierarchically structured name spaces.

Strengthened the possibility property for resumption so that it could have detected the problem with ServerResume

Fixed ServerResume to check for ServerHello instead of making a new NB

Exchanged the M and SID fields of the FINISHED messages to simplify proofs; deleted unused theorems

Exchanged the M and SID fields of the FINISHED messages to simplify proofs

Auto update

SYNC

Removed "browse.tex".

Added section describing the theory browser.

Updated usage information for tool "usedir".

Theory browser stuff has been moved to "present.tex".

obsolete;

ISABELLE_USEDIR_OPTIONS="-i true"

Changed html data directory and names of graph files.

There is now one single option -i for generating theory browsing information instead of the two options -h and -g .

Modified some links.

Client, Server certificates now sent using the separate Certificate rule, simplifying ServerHello and ClientKeyExch. Resumption no longer needs its own version of ServerHello. Proofs run nearly three minutes faster.

tuned;

superficial;

obsolete;

margin 76 (2nd try :-);

fixed href to html library;

improved warning;

default margin 76 (to accomodate warning and error default output);

Step_tac -> Safe_tac

Much tidying including step_tac -> clarify_tac or safe_tac; sometimes used qed_spec_mp

Step_tac -> Safe_tac

Much tidying including "qed" instead of result(), and even qed_spec_mp, and Safe_tac instead of step_tac

Previously loaded the WRONG THEORY, ignoring Confluence...

Now using qed_spec_mp

result() -> qed; Step_tac -> Safe_tac

Step_tac -> Safe_tac

Renamed XA, XB to PA, PB and removed the certificate from Client Verify