nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

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

SFT: Rename Lambda to LambdaTerms, rename constants to match Lambda, remove smt proofs.
2011-12-21, by Cezary Kaliszyk
Remove transitivity from the definition of One_star and show it instead.
2011-12-21, by Cezary Kaliszyk
Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.
2011-12-21, by Cezary Kaliszyk
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
2011-12-20, by Cezary Kaliszyk
Update Quotient FIXME-TODO, some issues were already fixed.
2011-12-20, by Cezary Kaliszyk
Added an initial version of qpaper-jv and a TODO of things to write about.
2011-12-20, by Cezary Kaliszyk
Remove 'HERE1' and 'HERE3'.
2011-12-20, by Cezary Kaliszyk
Lift substitution of an Abstraction for BetaCR :)
2011-12-20, by Cezary Kaliszyk
Tuned renaming
2011-12-20, by Cezary Kaliszyk
Retry Beta using a reduction relation and its reflexive-symmetric-transitive closure.
2011-12-19, by Cezary Kaliszyk
Disproved the property described as 'Tzevelakos'.
2011-12-19, by Cezary Kaliszyk
partially localised the parsing process using functions fron Datatype
2011-12-18, by Christian Urban

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

nominal2