nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Nominal/nominal_dt_rawfuns.ML

2010-10-17	Christian Urban	all tests work again	file \| diff \| annotate
2010-10-14	Christian Urban	major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)	file \| diff \| annotate
2010-09-10	Christian Urban	tuned (to conform with indentation policy of Markus)	file \| diff \| annotate
2010-09-03	Christian Urban	made the fv-definition aggree more with alpha (needed in the support proofs)	file \| diff \| annotate
2010-08-26	Christian Urban	corrected bug with fv-function generation (that was the problem with recursive binders)	file \| diff \| annotate
2010-08-25	Christian Urban	can now deal with type variables in nominal datatype definitions	file \| diff \| annotate
2010-08-17	Christian Urban	improved runtime slightly, by constructing an explicit size measure for the function definitions	file \| diff \| annotate
2010-08-17	Christian Urban	more tuning of the code	file \| diff \| annotate
2010-08-17	Christian Urban	improved code	file \| diff \| annotate
2010-07-29	Christian Urban	equivariance for size	file \| diff \| annotate
2010-07-27	Christian Urban	cleaned up a bit Abs.thy	file \| diff \| annotate
2010-07-27	Christian Urban	fixed order of fold_union to make alpha and fv agree	file \| diff \| annotate
2010-07-19	Christian Urban	minor polishing	file \| diff \| annotate
2010-06-22	Christian Urban	cleaned up the FSet (noise was introduced by error)	file \| diff \| annotate
2010-06-07	Christian Urban	work on transitivity proof	file \| diff \| annotate
2010-06-03	Christian Urban	fixed problem with eqvt proofs	file \| diff \| annotate
2010-06-02	Christian Urban	fixed problem with bn_info	file \| diff \| annotate
2010-06-01	Christian Urban	smaller code for raw-eqvt proofs	file \| diff \| annotate
2010-05-31	Christian Urban	all raw definitions are defined using function	file \| diff \| annotate
2010-05-24	Christian Urban	tuned	file \| diff \| annotate
2010-05-24	Christian Urban	alpha works now	file \| diff \| annotate
2010-05-23	Christian Urban	started to work on alpha	file \| diff \| annotate
2010-05-22	Christian Urban	properly exported bn_descr	file \| diff \| annotate
2010-05-21	Christian Urban	hving a working fv-definition without the export	file \| diff \| annotate
2010-05-21	Christian Urban	tuned	file \| diff \| annotate
2010-05-20	Christian Urban	tuned	file \| diff \| annotate
2010-05-20	Christian Urban	moved some mk_union and mk_diff into the library	file \| diff \| annotate
2010-05-20	Christian Urban	new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files	file \| diff \| annotate

less more (0) tip

nominal2

RSS Atom