renamed RuleContext to ContextRules;

\usepackage{textcomp}, \usepackage{marvosym};

renamed rule_context.ML to context_rules.ML;

setup "rules" method;

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;