2001-12-06 wenzelm 2001-12-06 * Pure/obtain: "thesis" now internal (use ?thesis); * Pure: generic 'sym' / 'symmetric' attributes; * Provers/classical: 'swapped' attribute; * HOL: proper rules less_induct and wf_induct_rule;
2001-12-06 wenzelm 2001-12-06 Syntax.internal thesis;
2001-12-06 wenzelm 2001-12-06 tuned xtra_netpair;
2001-12-06 wenzelm 2001-12-06 clarified sym_del;
2001-12-06 wenzelm 2001-12-06 added 'swapped' attribute; tuned xtra_netpair; tuned;
2001-12-06 wenzelm 2001-12-06 added the_mk_cases;
2001-12-06 wenzelm 2001-12-06 tuned;
2001-12-06 wenzelm 2001-12-06 renamed Finite to Finite_Set;
2001-12-06 wenzelm 2001-12-06 less_induct, wf_induct_rule;
2001-12-06 wenzelm 2001-12-06 renamed theory Finite to Finite_Set and converted;
2001-12-06 wenzelm 2001-12-06 this material already part of HOL/Set.thy;
2001-12-05 wenzelm 2001-12-05 sym [sym];
2001-12-05 wenzelm 2001-12-05 tuned;
2001-12-05 wenzelm 2001-12-05 iff;
2001-12-05 wenzelm 2001-12-05 updated;
2001-12-05 wenzelm 2001-12-05 adapted intr/elim uses;
2001-12-05 wenzelm 2001-12-05 eliminated old use of intro/elim method; tuned;
2001-12-05 wenzelm 2001-12-05 simplified proof (no longer use swapped rules);
2001-12-05 wenzelm 2001-12-05 fixed intro steps;
2001-12-05 wenzelm 2001-12-05 tuned declarations (rules, sym, etc.);
2001-12-05 wenzelm 2001-12-05 removed unused functionality (weight etc.);
2001-12-05 wenzelm 2001-12-05 simple version of 'intro' and 'elim' method; use ContextRules.find_rules;
2001-12-05 wenzelm 2001-12-05 added 'print_rules' command;
2001-12-05 wenzelm 2001-12-05 added print_rules;
2001-12-05 wenzelm 2001-12-05 simplified NetRules;
2001-12-05 wenzelm 2001-12-05 export low-level addXXs; find_rules interface;
2001-12-05 wenzelm 2001-12-05 added 'sym' and 'symmetric' atts;
2001-12-05 wenzelm 2001-12-05 removed bang_args;
2001-12-05 wenzelm 2001-12-05 'symmetric' attribute moved to Pure/calculation.ML;
2001-12-05 wenzelm 2001-12-05 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;
2001-12-05 wenzelm 2001-12-05 iff?: refer to Pure/ContextRules;
2001-12-05 wenzelm 2001-12-05 ContextRules.intro_bang_global;
2001-12-05 wenzelm 2001-12-05 added add_rule, del_rule;
2001-12-05 wenzelm 2001-12-05 tuned declarations;
2001-12-05 wenzelm 2001-12-05 tuned;
2001-12-05 wenzelm 2001-12-05 added ex/First_Order_Logic.thy, ex/document/root.tex;
2001-12-05 wenzelm 2001-12-05 added First_Order_Logic.thy;
2001-12-05 wenzelm 2001-12-05 sym declarations; tuned declarations;
2001-12-05 wenzelm 2001-12-05 removed declaration of disjI1, disjI2 (already done in IFOL);
2001-12-05 wenzelm 2001-12-05 removed AddXIs, AddXEs, AddXDs;
2001-12-05 wenzelm 2001-12-05 updated;
2001-12-05 wenzelm 2001-12-05 * Pure/Provers/classical: simplified integration with pure rule attributes and methods;
2001-12-04 wenzelm 2001-12-04 reactivate tracing markup;
2001-12-04 wenzelm 2001-12-04 made SML/NJ happy;
2001-12-04 wenzelm 2001-12-04 made slightly more robust;
2001-12-04 wenzelm 2001-12-04 added Higher_Order_Logic.thy;
2001-12-04 wenzelm 2001-12-04 rules_tac: SELECT_GOAL!!; tuned;
2001-12-04 wenzelm 2001-12-04 disable markup of tracing output (tmp?);
2001-12-04 wenzelm 2001-12-04 \usepackage{textcomp};
2001-12-04 wenzelm 2001-12-04 removed \newcommand{\isasymone};
2001-12-04 wenzelm 2001-12-04 hyp_subst_tac';
2001-12-04 wenzelm 2001-12-04 setup "rules" method;
2001-12-04 wenzelm 2001-12-04 no need for hyp_subst_tac' (!?);
2001-12-04 wenzelm 2001-12-04 renamed RuleContext to ContextRules;
2001-12-04 wenzelm 2001-12-04 \usepackage{textcomp}, \usepackage{marvosym};
2001-12-03 wenzelm 2001-12-03 renamed rule_context.ML to context_rules.ML;
2001-12-03 wenzelm 2001-12-03 setup "rules" method;
2001-12-03 wenzelm 2001-12-03 interface for wrappers;
2001-12-03 wenzelm 2001-12-03 added "rules" method;
2001-12-03 wenzelm 2001-12-03 removed questionable init_gensym;