isabelle: File revisions

src/HOL/simpdata.ML

2007-07-29	wenzelm	2007-07-29	simplified ResAtpset via NamedThmsFun; proper simproc_setup for "neq", "let_simp";	file \| diff \| annotate
2007-06-02	webertj	2007-06-02	refute_tac made more deterministic	file \| diff \| annotate
2007-05-06	haftmann	2007-05-06	tuned	file \| diff \| annotate
2007-01-21	wenzelm	2007-01-21	simplified ML setup;	file \| diff \| annotate
2007-01-20	wenzelm	2007-01-20	added @{clasimpset};	file \| diff \| annotate
2006-12-06	wenzelm	2006-12-06	simplified ML bindings -- moved to HOL.thy; removed confusing simpset_basic/simplify;	file \| diff \| annotate
2006-11-27	haftmann	2006-11-27	introduced Simpdata structure	file \| diff \| annotate
2006-11-12	wenzelm	2006-11-12	mk_atomize: careful matching against rules admits overloading;	file \| diff \| annotate
2006-11-03	haftmann	2006-11-03	re-added simpdata.ML	file \| diff \| annotate
2006-10-16	haftmann	2006-10-16	slight cleanup	file \| diff \| annotate
2006-10-11	haftmann	2006-10-11	cleaned up HOL bootstrap	file \| diff \| annotate
2006-10-10	haftmann	2006-10-10	cleanup basic HOL bootstrap	file \| diff \| annotate
2006-10-10	haftmann	2006-10-10	fixed typo	file \| diff \| annotate
2006-10-07	wenzelm	2006-10-07	tuned;	file \| diff \| annotate
2006-07-26	webertj	2006-07-26	linear arithmetic splits certain operators (e.g. min, max, abs)	file \| diff \| annotate
2006-07-11	wenzelm	2006-07-11	let_simproc: activate Variable.import;	file \| diff \| annotate
2006-07-08	wenzelm	2006-07-08	Goal.prove_global;	file \| diff \| annotate
2006-07-05	schirmer	2006-07-05	fixed let-simproc ----------------------------------------------------------------------	file \| diff \| annotate
2006-04-26	wenzelm	2006-04-26	removed obsolete expand_case_tac;	file \| diff \| annotate
2006-01-19	wenzelm	2006-01-19	setup: theory -> theory;	file \| diff \| annotate
2005-12-31	wenzelm	2005-12-31	removed obsolete Provers/make_elim.ML;	file \| diff \| annotate
2005-12-14	paulson	2005-12-14	deleted redundant (looping!) simprule	file \| diff \| annotate
2005-12-01	wenzelm	2005-12-01	unfold_tac: static evaluation of simpset;	file \| diff \| annotate
2005-11-16	wenzelm	2005-11-16	Term.betapply;	file \| diff \| annotate
2005-10-25	wenzelm	2005-10-25	avoid legacy goals;	file \| diff \| annotate
2005-10-21	wenzelm	2005-10-21	OldGoals;	file \| diff \| annotate
2005-10-18	wenzelm	2005-10-18	Simplifier.theory_context;	file \| diff \| annotate
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

isabelle

RSS Atom