Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-300
-100
-50
-30
+30
+50
+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.
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
Define lifted perms.
2010-02-24, by Cezary Kaliszyk
merged
2010-02-24, by Christian Urban
parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24, by Christian Urban
With permute_rsp we can lift the instance proofs :).
2010-02-24, by Cezary Kaliszyk
Note the instance proofs, since they can be easily lifted.
2010-02-24, by Cezary Kaliszyk
More refactoring and removed references to the global simpset in Perm.
2010-02-24, by Cezary Kaliszyk
Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24, by Cezary Kaliszyk
Regularize finite support proof for trm1
2010-02-24, by Cezary Kaliszyk
Made the fv-supp proof much more straightforward.
2010-02-24, by Cezary Kaliszyk
Regularize the proofs about finite support.
2010-02-24, by Cezary Kaliszyk
Respects of permute and constructors.
2010-02-24, by Cezary Kaliszyk
Generate fv_rsp automatically.
2010-02-24, by Cezary Kaliszyk
less
more
|
(0)
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
tip