src/HOL/HOL_lemmas.ML
2001-01-31 oheimb 2001-01-31 shortened proof of some1_equality
2000-12-23 wenzelm 2000-12-23 tuned comment;
2000-11-10 wenzelm 2000-11-10 axclass power moved to Nat.thy;
2000-10-17 paulson 2000-10-17 renaming of contrapos rules
2000-10-09 nipkow 2000-10-09 ex_someI -> someI_ex
2000-10-09 nipkow 2000-10-09 @ -> SOME
2000-09-22 wenzelm 2000-09-22 tuned comments;
2000-09-15 wenzelm 2000-09-15 fixed someI2_ex;
2000-09-15 paulson 2000-09-15 the final renaming: selectI -> someI
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-05 wenzelm 2000-09-05 improved meson setup;
2000-08-30 nipkow 2000-08-30 Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.
2000-08-04 wenzelm 2000-08-04 removed stac (now exported by HypsubstFun);
2000-07-21 nipkow 2000-07-21 added ex_someI
2000-06-28 paulson 2000-06-28 rev_notE now makes strong elim rules; tidied the file
2000-06-13 wenzelm 2000-06-13 qed_spec_mp: strip_shyps_warning;
2000-05-24 paulson 2000-05-24 some lemmas about plus_ac0
2000-03-20 paulson 2000-03-20 tidied
2000-02-22 wenzelm 2000-02-22 removed case_split thm binding;
1999-10-19 wenzelm 1999-10-19 qed_spec_mp is a mess;
1999-10-11 wenzelm 1999-10-11 bind_thm "ccontr";
1999-09-29 wenzelm 1999-09-29 bind_thm ("case_split", case_split_thm);
1999-09-28 paulson 1999-09-28 more tidying
1999-09-21 wenzelm 1999-09-21 removed "case" thm;
1999-09-09 oheimb 1999-09-09 minor change to smp_tac
1999-09-06 oheimb 1999-09-06 added smp_tac
1999-09-01 wenzelm 1999-09-01 bind_thm "case";
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;