isabelle: File revisions

src/Pure/conv.ML

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