2001-10-17 wenzelm 2001-10-17 tuned comments;
2001-10-17 wenzelm 2001-10-17 added mk_UNIV;
2001-10-17 wenzelm 2001-10-17 tuned;
2001-10-16 wenzelm 2001-10-16 simplified exporter interface;
2001-10-16 wenzelm 2001-10-16 added implies_intr_goals;
2001-10-16 wenzelm 2001-10-16 tuned;
2001-10-16 berghofe 2001-10-16 Tuned.
2001-10-16 berghofe 2001-10-16 Removed exit command from end of main method.
2001-10-16 berghofe 2001-10-16 PS method now calculates layout using default font metrics.
2001-10-16 berghofe 2001-10-16 Inserted table for character widths.
2001-10-16 wenzelm 2001-10-16 tuned induction proofs;
2001-10-16 wenzelm 2001-10-16 dest_env: norm_term on rhs;
2001-10-16 wenzelm 2001-10-16 typedef: export result;
2001-10-16 wenzelm 2001-10-16 ignore typedef result;
2001-10-16 wenzelm 2001-10-16 declare projected induction rules stemming from nested recursion;
2001-10-16 wenzelm 2001-10-16 TypedefPackage.add_typedef_no_result;
2001-10-16 wenzelm 2001-10-16 tuned;
2001-10-16 wenzelm 2001-10-16 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);
2001-10-16 wenzelm 2001-10-16 option -o FILE --output to FILE (ps, eps, pdf);
2001-10-16 wenzelm 2001-10-16 ISABELLE_EPSTOPDF="epstopdf";
2001-10-16 berghofe 2001-10-16 Font metrics used for batch mode layout (without X11 connection).
2001-10-16 berghofe 2001-10-16 Added support for batch mode layout (without X11 connection).
2001-10-16 wenzelm 2001-10-16 tuned;
2001-10-16 wenzelm 2001-10-16 improved induct;
2001-10-16 wenzelm 2001-10-16 be more careful about token class markers;
2001-10-16 wenzelm 2001-10-16 proper order of kind names;
2001-10-16 wenzelm 2001-10-16 support impromptu terminology of cases parameters;
2001-10-16 wenzelm 2001-10-16 parser for underscore (actually a symbolic identifier!);
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;