2000-11-06 wenzelm 2000-11-06 inductive_atomize, inductive_rulify;
2000-11-06 wenzelm 2000-11-06 * Isar/HOL: method 'induct' now handles non-atomic goals; as a consequence, it is no longer monotonic wrt. the local goal context (which is now passed through the inductive cases);
2000-11-06 wenzelm 2000-11-06 tuned atomize_goal;
2000-11-06 paulson 2000-11-06 minor modifications for new Springer style
2000-11-06 paulson 2000-11-06 minor changes
2000-11-06 paulson 2000-11-06 auto update
2000-11-06 nipkow 2000-11-06 *** empty log message ***
2000-11-04 wenzelm 2000-11-04 updated;
2000-11-04 wenzelm 2000-11-04 tuned method "rule" and "default";
2000-11-04 wenzelm 2000-11-04 isamarkup: handle % in input;
2000-11-04 wenzelm 2000-11-04 tuned;
2000-11-04 wenzelm 2000-11-04 misc stuff;
2000-11-03 wenzelm 2000-11-03 tuned;
2000-11-03 wenzelm 2000-11-03 proper setup of "parallel"; removed unused rules;
2000-11-03 wenzelm 2000-11-03 tuned notation;
2000-11-03 wenzelm 2000-11-03 adapted "obtain" proofs;
2000-11-03 wenzelm 2000-11-03 provide case names for rev_induct, rev_cases;
2000-11-03 wenzelm 2000-11-03 rev_exhaust: rulify;
2000-11-03 wenzelm 2000-11-03 removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-11-03 wenzelm 2000-11-03 "atomize" for classical tactics;
2000-11-03 wenzelm 2000-11-03 atomize: all automated tactics that "solve" goals;
2000-11-03 wenzelm 2000-11-03 fixed two obscurities of "fix": predeclare_terms;
2000-11-03 wenzelm 2000-11-03 tuned names;
2000-11-03 wenzelm 2000-11-03 improved handling of "that": insert into goal, only declare as Pure "intro"; eliminated functor;
2000-11-03 wenzelm 2000-11-03 assumption / finish: handle non-atomic assumptions from context as well;
2000-11-03 wenzelm 2000-11-03 added atomic_judgment;
2000-11-03 wenzelm 2000-11-03 structure Obtain = Obtain;
2000-11-03 paulson 2000-11-03 new lemma card_Diff2_less for mulilated chess board
2000-11-03 nipkow 2000-11-03 *** empty log message ***
2000-11-03 nipkow 2000-11-03 *** empty log message ***
2000-11-03 nipkow 2000-11-03 *** empty log message ***
2000-11-03 paulson 2000-11-03 the section command will belong to the new file
2000-11-03 paulson 2000-11-03 advanced induction examples
2000-11-03 paulson 2000-11-03 auto update?
2000-11-03 paulson 2000-11-03 replaced Acc.thy by Advanced.thy
2000-11-02 paulson 2000-11-02 no longer needed: too complicated an example
2000-11-02 nipkow 2000-11-02 *** empty log message ***
2000-11-02 paulson 2000-11-02 auto generated
2000-10-31 wenzelm 2000-10-31 tuned goal output;
2000-10-31 nipkow 2000-10-31 *** empty log message ***
2000-10-31 nipkow 2000-10-31 *** empty log message ***
2000-10-30 wenzelm 2000-10-30 updated;
2000-10-30 wenzelm 2000-10-30 tuned goals output;
2000-10-30 wenzelm 2000-10-30 improved statement bindings for props; tuned;
2000-10-30 wenzelm 2000-10-30 converse: syntax \<inverse>;
2000-10-30 wenzelm 2000-10-30 tuned;
2000-10-30 wenzelm 2000-10-30 added ex/PER.thy;
2000-10-30 wenzelm 2000-10-30 improved doc of "subgoals" antiquotation;
2000-10-30 wenzelm 2000-10-30 replaced \isasymmacron by \isasyminverse;
2000-10-30 wenzelm 2000-10-30 tuned tex template;
2000-10-30 wenzelm 2000-10-30 Partial equivalence relations (leftover from HOL/Quot);
2000-10-30 nipkow 2000-10-30 added antiq. subgoals
2000-10-30 nipkow 2000-10-30 Added antiquotation "subgoals".
2000-10-30 nipkow 2000-10-30 Mod because of additional parameters to pretty_goals.
2000-10-27 wenzelm 2000-10-27 back to 1.167, due to Emacs/CVS casualty!!;
2000-10-27 oheimb 2000-10-27 added instantiate_tac
2000-10-27 wenzelm 2000-10-27 *** empty log message ***
2000-10-27 kleing 2000-10-27 removed isabelle resources: are available from main pages
2000-10-27 kleing 2000-10-27 cleanup, looks ok now with konqueror, too
2000-10-26 nipkow 2000-10-26 *** empty log message ***