Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
merged
2010-03-02, by Christian Urban
added some more examples from Peter Sewell's bestiary
2010-03-02, by Christian Urban
merge
2010-03-02, by Cezary Kaliszyk
Minor
2010-03-02, by Cezary Kaliszyk
Working bv_eqvt
2010-03-02, by Cezary Kaliszyk
Moving wrappers out of Lift.
2010-03-02, by Cezary Kaliszyk
merged
2010-03-02, by Christian Urban
added distinctness of perms
2010-03-02, by Christian Urban
updated (added lemma about commuting permutations)
2010-03-02, by Christian Urban
Change type schemes to name set.
2010-03-02, by Cezary Kaliszyk
More fixes for new alpha, the whole lift script should now work again.
2010-03-02, by Cezary Kaliszyk
Length fix for nested recursions.
2010-03-02, by Cezary Kaliszyk
Fix equivp.
2010-03-02, by Cezary Kaliszyk
Fixed eqvt code.
2010-03-02, by Cezary Kaliszyk
most tests work - the ones that do not I commented out
2010-03-02, by Christian Urban
merge
2010-03-02, by Cezary Kaliszyk
Add a check of fv_functions.
2010-03-02, by Cezary Kaliszyk
some tuning
2010-03-02, by Christian Urban
Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02, by Cezary Kaliszyk
merged
2010-03-02, by Christian Urban
rawified the bind specs (ready to be used now)
2010-03-02, by Christian Urban
merge
2010-03-01, by Cezary Kaliszyk
Trying to prove equivariance.
2010-03-01, by Cezary Kaliszyk
modified for new binding format - hope it is the intended one
2010-03-01, by Christian Urban
further code-refactoring in the parser
2010-03-01, by Christian Urban
The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01, by Cezary Kaliszyk
slight simplification of the raw-decl generation
2010-03-01, by Christian Urban
Example that shows that current alpha is wrong.
2010-03-01, by Cezary Kaliszyk
added example from my phd
2010-03-01, by Christian Urban
streamlined parser
2010-02-27, by Christian Urban
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
2010-02-26, by Christian Urban
More about the general lifting procedure.
2010-02-26, by Cezary Kaliszyk
Update TODO
2010-02-26, by Cezary Kaliszyk
Progress with general lifting procedure.
2010-02-26, by Cezary Kaliszyk
RSP of perms can be shown in one go.
2010-02-26, by Cezary Kaliszyk
Change in signature of prove_const_rsp for general lifting.
2010-02-26, by Cezary Kaliszyk
Permutation and FV_Alpha interface change.
2010-02-26, by Cezary Kaliszyk
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-26, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Preparing the generalized lifting procedure
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
added ott-example about Leroy96
2010-02-25, by Christian Urban
Forgot to add one file.
2010-02-25, by Cezary Kaliszyk
Split Terms into separate files and add them to tests.
2010-02-25, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
a few simplifications
2010-02-25, by Christian Urban
first attempt to make sense out of the core-haskell definition
2010-02-25, by Christian Urban
Code for proving eqvt, still in Terms.
2010-02-25, by Cezary Kaliszyk
Use eqvt infrastructure.
2010-02-25, by Cezary Kaliszyk
Simple function eqvt code.
2010-02-25, by Cezary Kaliszyk
added IsaMakefile...but so far included only a test for the parser
2010-02-25, by Christian Urban
moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25, by Christian Urban
merged
2010-02-25, by Christian Urban
moved Nominal to "toplevel"
2010-02-25, by Christian Urban
Export perm_frees.
2010-02-25, by Cezary Kaliszyk
Restructuring the code in Perm
2010-02-24, by Cezary Kaliszyk
Simplified and finised eqvt proofs for t1 and t5
2010-02-24, by Cezary Kaliszyk
merge
2010-02-24, by Cezary Kaliszyk
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
+1000
tip