nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Nominal-General/Nominal2_Base.thy

2010-11-14	Christian Urban	moved most material fron Nominal2_FSet into the Nominal_Base theory	file \| diff \| annotate
2010-11-12	Christian Urban	automated permute_bn functions (raw ones first)	file \| diff \| annotate
2010-10-04	Christian Urban	changed to llncs	file \| diff \| annotate
2010-09-17	Christian Urban	updated to Isabelle Sept 16	file \| diff \| annotate
2010-09-10	Christian Urban	supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)	file \| diff \| annotate
2010-09-03	Christian Urban	moved everything out of Nominal_Supp	file \| diff \| annotate
2010-09-03	Christian Urban	got rid of Nominal_Atoms (folded into Nominal2_Base)	file \| diff \| annotate
2010-09-03	Christian Urban	cleaned a bit various thy-files in Nominal-General	file \| diff \| annotate
2010-07-22	Christian Urban	updated to new Isabelle; made FSet more "quiet"	file \| diff \| annotate
2010-06-03	Christian Urban	added uminus_eqvt	file \| diff \| annotate
2010-05-02	Christian Urban	slight tuning	file \| diff \| annotate
2010-04-30	Christian Urban	added lemmas establishing the support of finite sets of finitely supported elements	file \| diff \| annotate
2010-04-28	Christian Urban	use the more general type-class at_base	file \| diff \| annotate
2010-04-28	Christian Urban	deleted left-over code	file \| diff \| annotate
2010-04-28	Christian Urban	simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base	file \| diff \| annotate
2010-04-27	Christian Urban	moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base	file \| diff \| annotate
2010-04-24	Christian Urban	merged	file \| diff \| annotate
2010-04-22	Christian Urban	moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms	file \| diff \| annotate
2010-04-21	Christian Urban	tuned proofs	file \| diff \| annotate
2010-04-21	Christian Urban	moved some lemmas into the right places	file \| diff \| annotate
2010-04-19	Christian Urban	tuned proofs	file \| diff \| annotate
2010-04-14	Christian Urban	added a library for basic nominal functions; separated nominal_eqvt file	file \| diff \| annotate
2010-04-04	Christian Urban	separated general nominal theory into separate folder	file \| diff \| annotate \| base

less more (0) tip

nominal2

RSS Atom