2000-11-03 wenzelm proper setup of "parallel";
2000-11-03 wenzelm tuned notation;
2000-11-03 wenzelm adapted "obtain" proofs;
2000-11-03 wenzelm provide case names for rev_induct, rev_cases;
2000-11-03 wenzelm rev_exhaust: rulify;
2000-11-03 wenzelm removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-11-03 wenzelm "atomize" for classical tactics;
2000-11-03 wenzelm atomize: all automated tactics that "solve" goals;
2000-11-03 wenzelm fixed two obscurities of "fix": predeclare_terms;
2000-11-03 wenzelm tuned names;
2000-11-03 wenzelm improved handling of "that": insert into goal, only declare as Pure "intro";
2000-11-03 wenzelm assumption / finish: handle non-atomic assumptions from context as well;
2000-11-03 wenzelm added atomic_judgment;
2000-11-03 wenzelm structure Obtain = Obtain;
2000-11-03 paulson new lemma card_Diff2_less for mulilated chess board
2000-11-03 nipkow *** empty log message ***
2000-11-03 nipkow *** empty log message ***
2000-11-03 nipkow *** empty log message ***
2000-11-03 paulson the section command will belong to the new file
2000-11-03 paulson advanced induction examples
2000-11-03 paulson auto update?
2000-11-03 paulson replaced Acc.thy by Advanced.thy
2000-11-02 paulson no longer needed: too complicated an example
2000-11-02 nipkow *** empty log message ***
2000-11-02 paulson auto generated
2000-10-31 wenzelm tuned goal output;
2000-10-31 nipkow *** empty log message ***
2000-10-31 nipkow *** empty log message ***
Loading...
(0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip