fixed intro steps;

tuned declarations (rules, sym, etc.);

removed unused functionality (weight etc.);

simple version of 'intro' and 'elim' method; use ContextRules.find_rules;

added 'print_rules' command;

added print_rules;

simplified NetRules;

export low-level addXXs; find_rules interface;

added 'sym' and 'symmetric' atts;

removed bang_args;

'symmetric' attribute moved to Pure/calculation.ML;

simplified (and clarified) integration with Pure/ContextRules; removed "extra" rules as separate slots, only keep xtra_netpair for single-step view of plain haz/safe rules;

iff?: refer to Pure/ContextRules;

ContextRules.intro_bang_global;

added add_rule, del_rule;

tuned declarations;

tuned;

added ex/First_Order_Logic.thy, ex/document/root.tex;

added First_Order_Logic.thy;

sym declarations; tuned declarations;

removed declaration of disjI1, disjI2 (already done in IFOL);

removed AddXIs, AddXEs, AddXDs;

updated;

* Pure/Provers/classical: simplified integration with pure rule attributes and methods;

reactivate tracing markup;

made SML/NJ happy;

made slightly more robust;

added Higher_Order_Logic.thy;

rules_tac: SELECT_GOAL!!; tuned;

disable markup of tracing output (tmp?);

\usepackage{textcomp};

removed \newcommand{\isasymone};

hyp_subst_tac';

setup "rules" method;

no need for hyp_subst_tac' (!?);

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;