2000-11-10 ago wenzelm FOL_basic_ss: simprocs moved to FOL_ss;
2000-11-10 ago wenzelm added atomize_eq;
2000-11-10 ago wenzelm val atomize = thms "atomize'";
2000-11-10 ago nipkow > etc
2000-11-10 ago nipkow new: > and >=
2000-11-10 ago nipkow rule inversion
2000-11-10 ago nipkow JMB -> JMPB. Email von Johannes Pfeifroth.
2000-11-09 ago wenzelm updated;
2000-11-09 ago wenzelm fixed \title: convert "_" to "-";
2000-11-08 ago wenzelm tuned isabelle environment;
2000-11-08 ago nipkow subgoals
2000-11-08 ago nipkow *** empty log message ***
2000-11-07 ago paulson better discussion of rule induction
2000-11-07 ago berghofe Thm.dest_abs now takes an additional argument.
2000-11-07 ago berghofe Moved rewriting functions from Thm to MetaSimplifier.
2000-11-07 ago berghofe - Moved rewriting functions to meta_simplifier.ML
2000-11-07 ago berghofe moved rewriting functions from Drule to MetaSimplifier
2000-11-07 ago berghofe - new theorems imp_cong and swap_prems_eq
2000-11-07 ago berghofe Added new file meta_simplifier.ML
2000-11-07 ago berghofe Moved meta simplification stuff from Thm to MetaSimplifier.
2000-11-07 ago berghofe Added type constraint in theorem "lift".
2000-11-07 ago nipkow *** empty log message ***
2000-11-06 ago wenzelm method 'induct' now handles non-atomic goals;
2000-11-06 ago wenzelm improved: 'induct' handle non-atomic goals;
2000-11-06 ago wenzelm make: open_parms argument;
2000-11-06 ago wenzelm RuleCases.make true;
2000-11-06 ago wenzelm added rewrite_goal_tac;
2000-11-06 ago wenzelm added typ_instance;
2000-11-06 ago wenzelm Sign.typ_instance;
2000-11-06 ago wenzelm inductive_atomize, inductive_rulify;
2000-11-06 ago wenzelm * Isar/HOL: method 'induct' now handles non-atomic goals; as a
2000-11-06 ago wenzelm tuned atomize_goal;
2000-11-06 ago paulson minor modifications for new Springer style
2000-11-06 ago paulson minor changes
2000-11-06 ago paulson auto update
2000-11-06 ago nipkow *** empty log message ***
2000-11-04 ago wenzelm updated;
2000-11-04 ago wenzelm tuned method "rule" and "default";
2000-11-04 ago wenzelm isamarkup: handle % in input;
2000-11-04 ago wenzelm tuned;
2000-11-04 ago wenzelm misc stuff;
2000-11-03 ago wenzelm tuned;
2000-11-03 ago wenzelm proper setup of "parallel";
2000-11-03 ago wenzelm tuned notation;
2000-11-03 ago wenzelm adapted "obtain" proofs;
2000-11-03 ago wenzelm provide case names for rev_induct, rev_cases;
2000-11-03 ago wenzelm rev_exhaust: rulify;
2000-11-03 ago wenzelm removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-11-03 ago wenzelm "atomize" for classical tactics;
2000-11-03 ago wenzelm atomize: all automated tactics that "solve" goals;
2000-11-03 ago wenzelm fixed two obscurities of "fix": predeclare_terms;
2000-11-03 ago wenzelm tuned names;
2000-11-03 ago wenzelm improved handling of "that": insert into goal, only declare as Pure "intro";
2000-11-03 ago wenzelm assumption / finish: handle non-atomic assumptions from context as well;
2000-11-03 ago wenzelm added atomic_judgment;
2000-11-03 ago wenzelm structure Obtain = Obtain;
2000-11-03 ago paulson new lemma card_Diff2_less for mulilated chess board
2000-11-03 ago nipkow *** empty log message ***
2000-11-03 ago nipkow *** empty log message ***
2000-11-03 ago nipkow *** empty log message ***