2001-12-08 wenzelm 2001-12-08 tuned print_goals interfaces;
2001-12-08 wenzelm 2001-12-08 added General/xml.ML;
2001-12-08 wenzelm 2001-12-08 Basic support for XML output.
2001-12-07 paulson 2001-12-07 Slightly generalized the agents' knowledge theorems
2001-12-06 wenzelm 2001-12-06 added default_type;
2001-12-06 wenzelm 2001-12-06 tuned line breaks in HTML source;
2001-12-06 wenzelm 2001-12-06 fixed dest atts;
2001-12-06 wenzelm 2001-12-06 refrain from peeking at tags;
2001-12-06 wenzelm 2001-12-06 include session graph;
2001-12-06 paulson 2001-12-06 replaced record_split by the cases method
2001-12-06 paulson 2001-12-06 intro and elim now require arguments
2001-12-06 paulson 2001-12-06 record extend and truncate exercises
2001-12-06 wenzelm 2001-12-06 use Main;
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;