2001-10-16 wenzelm 2001-10-16 allow empty set/type name;
2001-10-16 wenzelm 2001-10-16 simplified resolveq_cases_tac for cases, separate version for induct; divinate instantiation of induct rules; tuned;
2001-10-16 wenzelm 2001-10-16 tuned;
2001-10-15 kleing 2001-10-15 canonical 'cases'/'induct' rules for n-tuples (n=3..7)
2001-10-15 kleing 2001-10-15 canonical 'cases'/'induct' rules for n-tuples (n=3..7) (really belongs to theory Product_Type, but doesn't work there yet)
2001-10-15 wenzelm 2001-10-15 setsum syntax;
2001-10-15 wenzelm 2001-10-15 intro! and elim! rules;
2001-10-15 wenzelm 2001-10-15 tuned NetRules;
2001-10-15 wenzelm 2001-10-15 Tactic.orderlist;
2001-10-15 wenzelm 2001-10-15 ObjectLogic.rulify;
2001-10-15 wenzelm 2001-10-15 Tactic.rewrite_cterm;
2001-10-15 wenzelm 2001-10-15 GPLed;
2001-10-15 wenzelm 2001-10-15 ring instead of ringS;
2001-10-15 wenzelm 2001-10-15 ring includes plus_ac0;
2001-10-15 wenzelm 2001-10-15 tuned;
2001-10-15 wenzelm 2001-10-15 support weight;
2001-10-15 wenzelm 2001-10-15 bang_args;
2001-10-15 wenzelm 2001-10-15 qualify some names;
2001-10-15 wenzelm 2001-10-15 map_nth_elem;
2001-10-15 oheimb 2001-10-15 renamed reset_locs to del_locs
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 added qed_spec_mp etc.;
2001-10-14 wenzelm 2001-10-14 unified rewrite/rewrite_cterm/simplify interface;
2001-10-14 wenzelm 2001-10-14 tuned rewrite/simplify interface;
2001-10-14 wenzelm 2001-10-14 improved atomize setup;
2001-10-14 wenzelm 2001-10-14 atomize_tac etc. moved to object_logic.ML;
2001-10-14 wenzelm 2001-10-14 use ObjectLogic;
2001-10-14 wenzelm 2001-10-14 added 'atomize' attribute;
2001-10-14 wenzelm 2001-10-14 tuned full_rewrite;
2001-10-14 wenzelm 2001-10-14 ObjectLogic.setup;
2001-10-14 wenzelm 2001-10-14 tuned;
2001-10-14 wenzelm 2001-10-14 added object_logic.ML;
2001-10-14 wenzelm 2001-10-14 fixed auto steps (due to changed atomize);
2001-10-14 wenzelm 2001-10-14 Specifics about common object-logics.
2001-10-14 wenzelm 2001-10-14 use ObjectLogic stuff;
2001-10-14 wenzelm 2001-10-14 "HOL.mono";
2001-10-14 wenzelm 2001-10-14 ObjectLogic.atomize_tac;
2001-10-14 wenzelm 2001-10-14 improved atomize setup;
2001-10-14 wenzelm 2001-10-14 removed Ord;
2001-10-14 wenzelm 2001-10-14 removed Ord.thy (now part of HOL.thy).
2001-10-14 wenzelm 2001-10-14 judgment Trueprop; proper declarations of atomize rules; incorporate theory Ord; proper section and text markup; tuned;
2001-10-14 wenzelm 2001-10-14 added ML bindings from former theory Ord;
2001-10-14 wenzelm 2001-10-14 eliminated atomize rules;
2001-10-14 wenzelm 2001-10-14 judgment Trueprop; proper declarations of atomize rules;
2001-10-13 wenzelm 2001-10-13 updated;
2001-10-13 wenzelm 2001-10-13 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
2001-10-13 wenzelm 2001-10-13 'morphisms' spec; tuned goal pattern for set;
2001-10-13 wenzelm 2001-10-13 tuned;
2001-10-13 wenzelm 2001-10-13 generic theorem kinds;
2001-10-13 wenzelm 2001-10-13 generic theorem kinds ("theorem", "lemma" etc.);
2001-10-13 wenzelm 2001-10-13 IsarThy.theorem_i Drule.internalK;
2001-10-13 wenzelm 2001-10-13 Drule.tag_internal;
2001-10-13 wenzelm 2001-10-13 * Pure: added 'corollary' command;
2001-10-12 berghofe 2001-10-12 Tuned comment.
2001-10-12 berghofe 2001-10-12 - Exported goals_conv and fconv_rule - Added forall_conv
2001-10-12 wenzelm 2001-10-12 removed vars_of, concls_of; removed additional rule instantiation argument; proper enumeration of type rules; append possibilities of set and type rules (analogous to elim-intro in 'rule');
2001-10-12 wenzelm 2001-10-12 declare impE iffD1 iffD2 ad elim of Pure;
2001-10-12 wenzelm 2001-10-12 removed lookups count; always try headless rules;
2001-10-12 wenzelm 2001-10-12 added make_thm (sort-of);