nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Nominal/Ex/Lambda.thy

2010-11-10	Christian Urban	adapted to changes by Florian on the quotient package and removed local fix for function package	file \| diff \| annotate
2010-09-29	Christian Urban	simplified exhaust proofs	file \| diff \| annotate
2010-09-29	Christian Urban	test with induct_schema for simpler strong_ind proofs	file \| diff \| annotate
2010-08-29	Christian Urban	renamed NewParser to Nominal2	file \| diff \| annotate
2010-08-27	Christian Urban	make copies of the "old" files	file \| diff \| annotate
2010-08-26	Christian Urban	"isabelle make test" makes all major examples....they work up to supp theorems (excluding)	file \| diff \| annotate
2010-08-25	Christian Urban	cleaned up (almost completely) the examples	file \| diff \| annotate
2010-08-25	Christian Urban	automatic lifting	file \| diff \| annotate
2010-08-25	Christian Urban	now every lemma lifts (even with type variables)	file \| diff \| annotate
2010-08-25	Christian Urban	can now deal with type variables in nominal datatype definitions	file \| diff \| annotate
2010-08-21	Christian Urban	nominal_datatypes with type variables do not work	file \| diff \| annotate
2010-08-21	Christian Urban	changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default	file \| diff \| annotate
2010-06-07	Christian Urban	work on transitivity proof	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Match_Lam defined on Quotient Level.	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	More on Function-defined subst.	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	merge	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Renamings.	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	merge (non-trival)	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Previously uncommited direct subst definition changes.	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Function experiments	file \| diff \| annotate
2010-05-19	Cezary Kaliszyk	more subst experiments	file \| diff \| annotate
2010-05-19	Cezary Kaliszyk	More subst experminets	file \| diff \| annotate
2010-05-18	Cezary Kaliszyk	more on subst	file \| diff \| annotate
2010-05-18	Cezary Kaliszyk	Single variable substitution	file \| diff \| annotate
2010-05-18	Cezary Kaliszyk	subst fix	file \| diff \| annotate
2010-05-18	Cezary Kaliszyk	subst experiments	file \| diff \| annotate
2010-05-12	Christian Urban	fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy	file \| diff \| annotate
2010-05-11	Cezary Kaliszyk	Include raw permutation definitions in eqvt	file \| diff \| annotate
2010-05-11	Cezary Kaliszyk	Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'	file \| diff \| annotate
2010-05-09	Christian Urban	cleaned up a bit the examples; added equivariance to all examples	file \| diff \| annotate

less more (0) -50 -30 tip

nominal2

RSS Atom