nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -1000 -300 -100 -60 +60 +100 +300 tip

trying new fcb in let/subst
2011-06-28, by Cezary Kaliszyk
Leftover only inj and eqvt
2011-06-28, by Cezary Kaliszyk
eapply fcb ok
2011-06-28, by Cezary Kaliszyk
Removed Inl and Inr
2011-06-28, by Cezary Kaliszyk
relaxed type in fcb
2011-06-28, by Christian Urban
fcb with explicit bn function
2011-06-28, by Christian Urban
added let-rec example
2011-06-28, by Christian Urban
Experiments with res
2011-06-28, by Cezary Kaliszyk
proved the fcb also for sets (no restriction yet)
2011-06-28, by Christian Urban
copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom
2011-06-28, by Christian Urban
streamlined the fcb-proof and made fcb1 a special case of fcb
2011-06-27, by Christian Urban
completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier)
2011-06-27, by Christian Urban
fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.
2011-06-27, by Christian Urban
renamed ds to dset (disagreement set)
2011-06-27, by Christian Urban
added small lemma about disagreement set
2011-06-27, by Christian Urban
merge
2011-06-27, by Cezary Kaliszyk
New-style fcb for multiple binders.
2011-06-27, by Cezary Kaliszyk
equality of lst_binder and a few helper lemmas
2011-06-27, by Cezary Kaliszyk
only one of the fcb precondistions are needed (probably the same with the perm-conditions)
2011-06-26, by Christian Urban
another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
2011-06-26, by Christian Urban
did all cases, except the multiple binder case
2011-06-25, by Christian Urban
an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders.
2011-06-25, by Christian Urban
except for the interated binder case, finished definition in Calssical.thy
2011-06-24, by Christian Urban
Make examples work with non-precompiled image
2011-06-24, by Cezary Kaliszyk
Remove Lambda_add.thy
2011-06-24, by Cezary Kaliszyk
The examples in Lambda_add can be defined by nominal_function directly
2011-06-24, by Cezary Kaliszyk
Theory name changes for JEdit
2011-06-24, by Cezary Kaliszyk
More usual names for substitution properties
2011-06-24, by Cezary Kaliszyk
Second Fixed Point Theorem
2011-06-24, by Cezary Kaliszyk
Speed-up the completeness proof.
2011-06-24, by Cezary Kaliszyk
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
2011-06-23, by Christian Urban
added file
2011-06-23, by Christian Urban
expanded the example
2011-06-23, by Christian Urban
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
2011-06-23, by Christian Urban
tuned
2011-06-22, by Christian Urban
deleted some dead code
2011-06-22, by Christian Urban
some rudimentary infrastructure for storing data about nominal datatypes
2011-06-22, by Christian Urban
constants with the same names
2011-06-22, by Cezary Kaliszyk
Quotients/TODO addtion
2011-06-22, by Cezary Kaliszyk
Minor
2011-06-21, by Cezary Kaliszyk
merge
2011-06-21, by Cezary Kaliszyk
spelling
2011-06-21, by Cezary Kaliszyk
merge
2011-06-20, by Cezary Kaliszyk
Abs_set_fcb
2011-06-20, by Cezary Kaliszyk
function for let-rec
2011-06-20, by Cezary Kaliszyk
TODO/minor
2011-06-20, by Cezary Kaliszyk
Move lst_fcb to Nominal2_Abs
2011-06-20, by Cezary Kaliszyk
More minor TODOs
2011-06-20, by Cezary Kaliszyk
Update TODO
2011-06-20, by Cezary Kaliszyk
Let/minor
2011-06-20, by Cezary Kaliszyk
Update Quotient/TODO and remove some attic code
2011-06-20, by Cezary Kaliszyk
merge
2011-06-19, by Cezary Kaliszyk
little on cps2
2011-06-19, by Cezary Kaliszyk
got rid of the boolean flag in the raw_equivariance function
2011-06-16, by Christian Urban
Fix
2011-06-16, by Cezary Kaliszyk
merge
2011-06-16, by Cezary Kaliszyk
CPS3 can be defined with eqvt_rhs.
2011-06-16, by Cezary Kaliszyk
moved for the moment CPS translations into the example directory
2011-06-16, by Christian Urban
merged
2011-06-16, by Christian Urban
added eqvt_at and invariant for boths sides of the equations
2011-06-16, by Christian Urban

less more | (0) -1000 -300 -100 -60 +60 +100 +300 tip

nominal2