interface for wrappers;

added "rules" method;

removed questionable init_gensym;

hyp_subst_tac';

use \<zero>, \<one>;

\renewcommand{\isasymzero}, \renewcommand{\isasymone};

updated;

HOLogic.read_cterm;

HOLogic.typeS;

removed dead code;

renamed class "term" to "type" (actually "HOL.type");

added zero--nine, euro; tuned some text symbols;

%\usepackage{textcomp} %\usepackage{marvosym}

* HOL: the class of all HOL types is now called "type" rather than "term"; INCOMPATIBILITY, need to adapt references to this type class in axclass/classes, instance/arities, and (usually rare) occurrences in typings (of consts etc.); internally the class is called "HOL.type", ML programs should refer to HOLogic.typeS;

*** empty log message ***

minor tweaks

*** empty log message ***

*** empty log message ***

*** empty log message ***

minor textual tweaks

*** empty log message ***

*** empty log message ***

export primitive netpairs; activate attributes;

RuleContext.intro_query_local;

rule context and attributes moved to rule_context.ML;

qualify_elem: do not qualify empty names ("");

tuned;

added deletion of rules; tuned;

general type of delete_tagged_brl; tuned;

most general type of delete/delete_term;

skip_proof: do not require quick_and_dirty in interactive mode;

support "_::foo" sort constraints;

removed unused simple_read_typ; read_typ, TypeExt.typ_of_term: map_sort argument;

added proof_to_theory';

Syntax.typ_of_term: pass intern sort fn;

Syntax.read_typ: pass intern sort fn;

* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode; * Pure/syntax: "x::_::foo" sort constraints;

theory data: removed obsolete finish method;

data: removed obsolete finish method;

name space for local thms (export cond_extern, qualified); improved internal naming of fixes;

print_state: up to 7 result names;

qualify imported facts; clarified read/cert_element; theory data: removed obsolete finish; tuned;

variant: preserve suffix of underscores (for skolem/internal names etc.);

join_rules RuleCases.save;

tuned declarations;

tuned;

make SML/NJ happy;

added Pure/Isar/rule_context.ML;

gcd_dvd1 and gcd_dvd2 proven simultaneously;

moved lemmas to theory Hilbert_Choice;

tuned; meson lemmas from Tools/meson.ML;

added remdups_rl;

clarified order of merge_lists';

clarified order in gen_merge_lists';

fixed SML/NJ error (!?);

use merge_lists, merge_alists;

Symtab.merge_multi'; tuned;

type variables: clarified "used" vs. "occ";

Library.gen_merge_lists';

clarified locale operations (rename, merge); tuned;

print_locale: expr;

added join, merge_multi('); tuned extend, make, merge;

merge_stamps: merge_lists' with reversed args;

gen_merge_lists;

added gen_merge_lists(') and merge_lists('); removed obsolete generic_extend, generic_merge, extend_list;

gen_merge_lists';

generic_merge;

converted simp lemmas;

tuned;

Extended match_proof to handle abstractions.

tuned;

improved ordering of evaluated elements;

time_use_thy "Locales";

Isar conversion

theory Locales temporarily disabled;

beginnings of actual locale expressions;

improved locale expression syntax;

locale expression import;

import locale expression;

tuned;

added uname; syntax for locale expressions (presently unused);

tuned;

thm "point.defs";

recovered original "make"; added "fields" operation; renamed "derived_defs" to "defs";

renamed "fields" to "flds" (avoid clash with new "fields" operation);

locale expressions;

use tracing function for trace output;

tracing_fn;

added tracing, tracing_fn;

Set.vimage;

got rid of theory Inverse_Image;

theory Inverse_Image converted and moved to Set;

tuned;

tuned;

fixed links etc.;

* HOL/record: cases/induct for more parts; * syntax: prefer later print_translation functions;

prefer later trfuns;

moved prefixes1, suffixes1 to library.ML;

trfuns *after* binder syntax;

added prefixes1, suffixes1;

print_depth 10;

derive cases/induct rules for ``more'' parts;

tuned;

Hyperreal

improved treatment of common result name;

tuned;

multi_theorem: common statement header (covers *all* results);

fixed comment; goal: unbind if multiple statements;

induct method: localize rews for rule;

Now handles different theorems with same name more gracefully.

Improved error message.

Added setup.