isabelle: File revisions

src/Pure/conv.ML

2010-08-23	haftmann	2010-08-23	tap_thy conversional	file \| diff \| annotate
2010-05-15	wenzelm	2010-05-15	incorporated further conversions and conversionals, after some minor tuning;	file \| diff \| annotate
2009-10-01	wenzelm	2009-10-01	moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;	file \| diff \| annotate
2009-02-26	boehmes	2009-02-26	Made then_conv and else_conv available as infix operations.	file \| diff \| annotate
2009-01-21	wenzelm	2009-01-21	removed Ids;	file \| diff \| annotate
2008-06-23	wenzelm	2008-06-23	Logic.is_all;	file \| diff \| annotate
2008-04-07	wenzelm	2008-04-07	abs_conv: extra argument for bound variable; renamed iterated forall_conv to params_conv; added forall_conv, implies_conv, implies_concl_conv, rewr_conv;	file \| diff \| annotate
2008-02-25	wenzelm	2008-02-25	tuned;	file \| diff \| annotate
2007-10-04	wenzelm	2007-10-04	abs_conv/forall_conv: proper context (avoid gensym); removed unused cache_conv;	file \| diff \| annotate
2007-07-08	wenzelm	2007-07-08	gensym: slightly more obscure prefix descreases probability of name clash;	file \| diff \| annotate
2007-07-05	wenzelm	2007-07-05	moved type conv to thm.ML; renamed Conv.is_refl to Thm.is_reflexive; misc tuning of basic conversions;	file \| diff \| annotate
2007-07-05	wenzelm	2007-07-05	tuned;	file \| diff \| annotate
2007-07-05	wenzelm	2007-07-05	else_conv: only handle THM \| CTERM \| TERM \| TYPE; prems_conv: no index; renamed goal_conv_rule to gconv_rule;	file \| diff \| annotate
2007-07-03	wenzelm	2007-07-03	removed obsolete goals_conv (cf. prems_conv); added efficient goal_conv_rule; tuned comments;	file \| diff \| annotate
2007-06-25	wenzelm	2007-06-25	made type conv pervasive; removed obsolete eta_conv (cf. Thm.eta_long_conv);	file \| diff \| annotate
2007-06-17	chaieb	2007-06-17	Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl	file \| diff \| annotate
2007-05-31	wenzelm	2007-05-31	moved aconvc to more_thm.ML;	file \| diff \| annotate
2007-05-19	chaieb	2007-05-19	added binop_conv, aconvc	file \| diff \| annotate
2007-05-11	wenzelm	2007-05-11	unified names: foo_conv;	file \| diff \| annotate
2007-05-10	wenzelm	2007-05-10	more conversions; tuned;	file \| diff \| annotate
2007-05-10	wenzelm	2007-05-10	Conversions: primitive equality reasoning (from drule.ML);	file \| diff \| annotate

isabelle

RSS Atom