2001-12-05 ago wenzelm export low-level addXXs;
2001-12-05 ago wenzelm added 'sym' and 'symmetric' atts;
2001-12-05 ago wenzelm removed bang_args;
2001-12-05 ago wenzelm 'symmetric' attribute moved to Pure/calculation.ML;
2001-12-05 ago wenzelm simplified (and clarified) integration with Pure/ContextRules;
2001-12-05 ago wenzelm iff?: refer to Pure/ContextRules;
2001-12-05 ago wenzelm ContextRules.intro_bang_global;
2001-12-05 ago wenzelm added add_rule, del_rule;
2001-12-05 ago wenzelm tuned declarations;
2001-12-05 ago wenzelm tuned;
2001-12-05 ago wenzelm added ex/First_Order_Logic.thy, ex/document/root.tex;
2001-12-05 ago wenzelm added First_Order_Logic.thy;
2001-12-05 ago wenzelm sym declarations;
2001-12-05 ago wenzelm removed declaration of disjI1, disjI2 (already done in IFOL);
2001-12-05 ago wenzelm removed AddXIs, AddXEs, AddXDs;
2001-12-05 ago wenzelm updated;
2001-12-05 ago wenzelm * Pure/Provers/classical: simplified integration with pure rule
2001-12-04 ago wenzelm reactivate tracing markup;
2001-12-04 ago wenzelm made SML/NJ happy;
2001-12-04 ago wenzelm made slightly more robust;
2001-12-04 ago wenzelm added Higher_Order_Logic.thy;
2001-12-04 ago wenzelm rules_tac: SELECT_GOAL!!;
2001-12-04 ago wenzelm disable markup of tracing output (tmp?);
2001-12-04 ago wenzelm \usepackage{textcomp};
2001-12-04 ago wenzelm removed \newcommand{\isasymone};
2001-12-04 ago wenzelm hyp_subst_tac';
2001-12-04 ago wenzelm setup "rules" method;
2001-12-04 ago wenzelm no need for hyp_subst_tac' (!?);
2001-12-04 ago wenzelm renamed RuleContext to ContextRules;
2001-12-04 ago wenzelm \usepackage{textcomp}, \usepackage{marvosym};
2001-12-03 ago wenzelm renamed rule_context.ML to context_rules.ML;
2001-12-03 ago wenzelm setup "rules" method;
2001-12-03 ago wenzelm interface for wrappers;
2001-12-03 ago wenzelm added "rules" method;
2001-12-03 ago wenzelm removed questionable init_gensym;
2001-12-03 ago wenzelm hyp_subst_tac';
2001-12-03 ago wenzelm use \<zero>, \<one>;
2001-12-03 ago wenzelm \renewcommand{\isasymzero}, \renewcommand{\isasymone};
2001-12-03 ago wenzelm updated;
2001-12-03 ago wenzelm HOLogic.read_cterm;
2001-12-03 ago wenzelm HOLogic.typeS;
2001-12-01 ago wenzelm removed dead code;
2001-12-01 ago wenzelm renamed class "term" to "type" (actually "HOL.type");
2001-12-01 ago wenzelm added zero--nine, euro;
2001-12-01 ago wenzelm %\usepackage{textcomp}
2001-12-01 ago wenzelm * HOL: the class of all HOL types is now called "type" rather than
2001-11-30 ago nipkow *** empty log message ***
2001-11-30 ago paulson minor tweaks
2001-11-29 ago nipkow *** empty log message ***
2001-11-29 ago nipkow *** empty log message ***
2001-11-29 ago nipkow *** empty log message ***
2001-11-29 ago paulson minor textual tweaks
2001-11-29 ago nipkow *** empty log message ***
2001-11-29 ago nipkow *** empty log message ***
2001-11-29 ago wenzelm export primitive netpairs;
2001-11-29 ago wenzelm RuleContext.intro_query_local;
2001-11-29 ago wenzelm rule context and attributes moved to rule_context.ML;
2001-11-29 ago wenzelm qualify_elem: do not qualify empty names ("");
2001-11-29 ago wenzelm tuned;
2001-11-29 ago wenzelm added deletion of rules;