oops, swap warnings;

record: tuned output;

ProtoPure.flexpair_def;

ProtoPure.flexpair_def;

merge: default to ProtoPure.thy;

ProtoPure.thy etc.;

tuned names; tuned prep_ext_merge;

self_ref: check_stale; moved pure stuff to pure_thy.ML;

eq_thm (from drule.ML);

added declared: T -> string -> bool; intern / extern;

Pure.thy;

ProtoPure.thy;

tuned; added print_data "theorems";

tuned;

removed add_thms_as_axms;

Init 'theorems' data. The Pure theories.

added pure_thy.ML;

tuned;

Modified comment.

Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!

HOL/Map

Added the new theory Map.

added record section;

Sign.name_of;

Sign.stamp_names_of;

improved typ parser, exported;

tuned;

hide id, stamps; added stamp_names_of, name_of; replaced make_draft by prep_ext; improved print_sg; tuned;

Sign.stamp_names_of;

added sort_wrt;

fixed prune of hidden short names;

tuned;

tuned;

certify: check_stale;

improved handling of draft signatures / theories; draft thms (and ctyps, cterms) are automatically promoted to real ones;

sg_ref: automatic adjustment of thms of draft theories;

commit;

made Poly/ML happy, but SML/NJ unhappy;

typo

Corrected alphabetical order of entries in signature.

Fixed the index entries for "recursion, general"

Many minor speedups: 1. Some use of rewriting with expand_ifs instead of addsplits[expand_if] 2. Faster proof of new_keys_not_used 3. New version of shrK_neq (no longer refers to "range")

New rewrite rules image_iff

Documented `addsplits'

make SML/NJ happy;

rm IOA TLA;

tuned types;

tuned sig;

reset global_names;

set global_names;

replaced ops by consts;

removed Dlist;

\label{simp-chap} -> chap:simplification Indexed "higher-order pattern"

fixed goal_XXX;

adapted to qualified names;

adapted to qualified names;

tuned; adapted to qualified names;

adapted to qualified names;

lookup long names of types;

tuned qualified names;

adapted to qualified names;

qualified names;

local;

Sign.base_name;

fixed types of add_XXX; tuned;

fixed types of add_XXX; added base_name; tuned exports; tuned output of sg;

tuned output;

adapted to qualified names;

Sign.base_name;

fixed types of add_XXX;

local;

local section; improved global, local;

addsplits

adapted to qualified names;

no longer tries bogus eta-contract involving aprops;

adapted to qualified names;

fixed RAW target;

(co) inductive / datatype package adapted to qualified names;

obselete 'end' hack;

global;

tuned "." syntax;

removed Classlib;

*** empty log message ***

setloop split_tac -> addsplits

Added error messages.

A lot of new comments

Eta-expanded a function decl to make sml/nj happy

Added "op" before "occs" to make sml/nj happy

New rewrite rules for simplifying conditionals

New trivial rewrites

New rewrite rules for simplifying conditionals

Better simplification eliminates a command from proof of psubset_card

New simprules imp_disj1,2 and some comments

Added image_eqI to simpset.

Removed image_eqI from simpset because of clash with neq_shrK.

AddIffs [all_not_in_conv];

global;

Modified comment.

New simprules imp_disj1, imp_disj2

New simprule diff_le_self, requiring a new proof of diff_diff_cancel

Removed comment.

tuned;

removed begin; added global section; added global_names flag (tmp), default true;

fixed prep_ext;

Simplified proof.

Simplified proof because of better simplifier.

Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).

added transfer: theory -> thm -> thm;

oops;

The simplifier has been improved a little: equations s=t which used to be rejected because of looping are now treated as (s=t) == True. The latter translation must be done outside of Thm because it involves the object-logic specific True. Therefore the simple loop test has been moved from Thm to Logic.

fixed dependencies;

transfer thy Ord_nat;

sevaral goals restated in mono.thy;

moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;

transfer InfDatatype.thy Limit_VfromE;

transfer CardinalArith.thy nat_into_Ord;

improved pretty_arity;

added merge_theories (new name arg);

fixed merge_theories;

revert to 1.3;

revert to 1.1;

Added last, butlast, dropped ttl.

lala

Eta-expansion of function declarations, for value polymorphism

remove merge_theories; merge_list: always prepares extend -- no longer supports aliasing merges;

make_draft replaced by prep_ext; improved print_data; merge now does trivial (absorptive) merges only; added nontriv_merge;

tuned;

eliminated aliasing merge: now always extends;

tuned comment;

improved print_data;

tuned; prepare ext;

slightly changed interfaces for oracles;

Added ack to Mateja Jamnik.

tuned;

tuned;

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;