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;