isabelle: File revisions

src/HOL/simpdata.ML

2005-10-17	wenzelm	2005-10-17	change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;	file \| diff \| annotate
2005-10-07	nipkow	2005-10-07	changes due to new neq_simproc in simpdata.ML	file \| diff \| annotate
2005-09-12	haftmann	2005-09-12	introduced new-style AList operations	file \| diff \| annotate
2005-08-31	wenzelm	2005-08-31	simp_implies: proper named infix;	file \| diff \| annotate
2005-08-02	wenzelm	2005-08-02	added unfold_tac (Simplifier.inherit_bounds);	file \| diff \| annotate
2005-08-02	ballarin	2005-08-02	Turned simp_implies into binary operator.	file \| diff \| annotate
2005-07-01	berghofe	2005-07-01	Implemented trick (due to Tobias Nipkow) for fine-tuning simplification of premises of congruence rules.	file \| diff \| annotate
2005-06-28	paulson	2005-06-28	Constant "If" is now local	file \| diff \| annotate
2005-03-03	skalberg	2005-03-03	Move towards standard functions.	file \| diff \| annotate
2005-02-13	skalberg	2005-02-13	Deleted Library.option type.	file \| diff \| annotate
2004-12-18	schirmer	2004-12-18	added simproc for Let	file \| diff \| annotate
2004-09-06	nipkow	2004-09-06	made mult_mono_thms generic.	file \| diff \| annotate
2004-05-14	paulson	2004-05-14	new atomize theorem	file \| diff \| annotate
2004-03-04	paulson	2004-03-04	new material from Avigad, and simplified treatment of division by 0	file \| diff \| annotate
2002-12-09	ballarin	2002-12-09	Fixed bug in simpdata.ML that prevented the use of congruence rules from a locale. (mk_meta_cong did wrongly convert metahyps to hyps)	file \| diff \| annotate
2002-09-30	berghofe	2002-09-30	Removed nRS again because extract_rews now takes care of preserving names.	file \| diff \| annotate
2002-09-19	nipkow	2002-09-19	preserve names of rewrite rules when transforming them	file \| diff \| annotate
2002-08-06	wenzelm	2002-08-06	sane interface for simprocs;	file \| diff \| annotate
2002-02-28	paulson	2002-02-28	fixing nat_combine_numerals simprocs (again) Theorem eq_cong2 moved from Integ/int_arith1.ML to simpdata.ML, where it will be available in all theories. Function simplify_meta_eq now makes the meta-equality first so that eq_cong2 will work properly.	file \| diff \| annotate
2002-01-12	wenzelm	2002-01-12	renamed forall_elim_vars_safe to gen_all;	file \| diff \| annotate
2001-12-17	nipkow	2001-12-17	mods due to mor powerful simprocs for 1-point rules (quantifier1).	file \| diff \| annotate
2001-12-12	nipkow	2001-12-12	Removed pointless backtracking from arith_tac	file \| diff \| annotate
2001-11-24	wenzelm	2001-11-24	converted simp lemmas;	file \| diff \| annotate
2001-11-23	wenzelm	2001-11-23	tuned;	file \| diff \| annotate
2001-11-03	wenzelm	2001-11-03	proper use of bind_thm(s);	file \| diff \| annotate
2001-10-04	wenzelm	2001-10-04	removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);	file \| diff \| annotate
2001-09-28	berghofe	2001-09-28	mksimps and mk_eq_True no longer raise THM exception.	file \| diff \| annotate
2001-08-31	berghofe	2001-08-31	Proof of True_implies_equals is stored with "open" derivation to facilitate simplification of proof terms.	file \| diff \| annotate
2001-07-25	paulson	2001-07-25	partial restructuring to reduce dependence on Axiom of Choice	file \| diff \| annotate
2001-07-20	wenzelm	2001-07-20	HOL_ss: the_eq_trivial, the_sym_eq_trivial;	file \| diff \| annotate
2001-05-31	oheimb	2001-05-31	streamlined addIffs/delIffs, added warnings	file \| diff \| annotate
2001-03-29	nipkow	2001-03-29	generalization of 1 point rules for ALL	file \| diff \| annotate
2001-03-23	nipkow	2001-03-23	added one point simprocs for bounded quantifiers	file \| diff \| annotate
2001-03-09	nipkow	2001-03-09	arith_tac now copes with propositional reasoning as well.	file \| diff \| annotate
2001-02-20	oheimb	2001-02-20	debugging: replaced gen_all by forall_elim_vars_safe	file \| diff \| annotate
2001-02-02	wenzelm	2001-02-02	added hol_simplify, hol_rewrite_cterm;	file \| diff \| annotate
2001-01-30	oheimb	2001-01-30	added if_def2	file \| diff \| annotate
2000-10-17	paulson	2000-10-17	renaming of contrapos rules	file \| diff \| annotate
2000-09-15	paulson	2000-09-15	renamed (most of...) the select rules	file \| diff \| annotate
2000-09-07	wenzelm	2000-09-07	eliminated rulify setup (now in Provers/rulify.ML);	file \| diff \| annotate
2000-09-06	wenzelm	2000-09-06	tuned;	file \| diff \| annotate
2000-09-06	nipkow	2000-09-06	imp_cong bound at thm level.	file \| diff \| annotate
2000-09-05	wenzelm	2000-09-05	iff declarations moved to clasimp.ML;	file \| diff \| annotate
2000-09-04	wenzelm	2000-09-04	added safe_mk_meta_eq;	file \| diff \| annotate
2000-09-02	wenzelm	2000-09-02	added 'iff del' att;	file \| diff \| annotate
2000-08-30	nipkow	2000-08-30	Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.	file \| diff \| annotate
2000-08-29	wenzelm	2000-08-29	cong setup now part of Simplifier;	file \| diff \| annotate
2000-08-03	paulson	2000-08-03	new theorem neq_commute	file \| diff \| annotate
2000-07-18	wenzelm	2000-07-18	* HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm;	file \| diff \| annotate
2000-06-28	paulson	2000-06-28	make_elim -> cla_make_elim; tidied	file \| diff \| annotate
2000-06-02	oheimb	2000-06-02	added eta_contract_eq, also to simpset	file \| diff \| annotate
2000-05-24	paulson	2000-05-24	installing the plus_ac0 simprules	file \| diff \| annotate
2000-03-31	wenzelm	2000-03-31	added cong atts;	file \| diff \| annotate
2000-03-31	wenzelm	2000-03-31	change_global/local_css move to Provers/clasimp.ML; fixed 'iff' att syntax; added 'cong' att;	file \| diff \| annotate
2000-03-15	wenzelm	2000-03-15	splitter setup;	file \| diff \| annotate
2000-01-07	paulson	2000-01-07	tidied parentheses	file \| diff \| annotate
1999-10-05	berghofe	1999-10-05	Rule not_not is now stored in theory (needed by Inductive).	file \| diff \| annotate
1999-09-29	wenzelm	1999-09-29	bind_thms;	file \| diff \| annotate
1999-09-28	paulson	1999-09-28	AC rules for equality	file \| diff \| annotate
1999-09-23	paulson	1999-09-23	tidied; added lemma restrict_to_left	file \| diff \| annotate

isabelle

RSS Atom