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.
build_eqvts works with recursive case if proper induction rule is used.
2010-03-15, by Cezary Kaliszyk
cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-15, by Cezary Kaliszyk
LF works with new alpha...?
2010-03-15, by Cezary Kaliszyk
explicit flag "cheat_equivp"
2010-03-15, by Cezary Kaliszyk
Prove alpha_gen_compose_eqvt
2010-03-15, by Cezary Kaliszyk
Use eqvt.
2010-03-15, by Cezary Kaliszyk
added preliminary test version....but Test works now
2010-03-15, by Christian Urban
added an eqvt-proof for bi
2010-03-15, by Christian Urban
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
2010-03-15, by Christian Urban
localised the typedef in Attic (requires new Isabelle)
2010-03-14, by Christian Urban
started supp-fv proofs (is going to work)
2010-03-13, by Christian Urban
Even with pattern simplified to a single clause, the supp equation doesn't seem true.
2010-03-12, by Cezary Kaliszyk
Still don't know how to prove supp=fv for simplest Let...
2010-03-12, by Cezary Kaliszyk
Do not fail if the finite support proof fails.
2010-03-11, by Cezary Kaliszyk
generalised the supp for atoms to all concrete atoms (not just names)
2010-03-11, by Christian Urban
support of atoms at the end of Abs.thy
2010-03-11, by Christian Urban
Trying to prove atom_image_fresh_swap
2010-03-11, by Cezary Kaliszyk
Finite_support proof no longer needed in LF.
2010-03-11, by Cezary Kaliszyk
Show that the new types are in finite support typeclass.
2010-03-11, by Cezary Kaliszyk
mk_supports_eq and supports_tac.
2010-03-11, by Cezary Kaliszyk
merge
2010-03-11, by Cezary Kaliszyk
Fixes for term1 for new alpha. Still not able to show support equations.
2010-03-11, by Cezary Kaliszyk
merged
2010-03-11, by Christian Urban
finally the proof that new and old alpha agree
2010-03-11, by Christian Urban
Remove "_raw" from lifted theorems.
2010-03-11, by Cezary Kaliszyk
looking at trm5_equivp
2010-03-11, by Cezary Kaliszyk
The cheats described explicitely.
2010-03-11, by Cezary Kaliszyk
The alpha5_eqvt tactic works if I manage to build the goal.
2010-03-11, by Cezary Kaliszyk
With the 4 cheats, all examples fully lift.
2010-03-11, by Cezary Kaliszyk
Lift alpha_bn_constants.
2010-03-11, by Cezary Kaliszyk
less
more
|
(0)
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
tip