added additional generic data;

Sign.print_data;

added init_data, get_data, put_data;

added data.ML;

Arbitrarily typed data.

Patch to avoid simplification of ~EX to ALL~ Also some better indentation

Two lemmas are already in List.

More lemmas, esp. ~Bex and ~Ball conversions.

Added neagtion rules for Ball and Bex. ZF/AC now fails to build. Larry to fix.

tuned;

browser info;

rearranged and added TLA

fixed extern; added str_of_classrel, str_of_arity, str_of_arity;

uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;

uses Sign.str_of_sort;

fixed dots;

print_goals: optional output of const types (set show_consts);

merge: drops path elements;

Absolute URL's for documentation

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.