Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-120
+120
+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.
Generalize Abs_eq_iff.
2010-03-27, by Cezary Kaliszyk
Minor fix.
2010-03-27, by Cezary Kaliszyk
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
2010-03-27, by Cezary Kaliszyk
Initial proof modifications for alpha_res
2010-03-27, by Cezary Kaliszyk
merge
2010-03-27, by Cezary Kaliszyk
Fv/Alpha now takes into account Alpha_Type given from the parser.
2010-03-27, by Cezary Kaliszyk
Minor cleaning.
2010-03-27, by Cezary Kaliszyk
merged
2010-03-27, by Christian Urban
more on the paper
2010-03-27, by Christian Urban
Removed some warnings.
2010-03-27, by Cezary Kaliszyk
merge
2010-03-26, by Cezary Kaliszyk
Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.
2010-03-26, by Cezary Kaliszyk
merged
2010-03-26, by Christian Urban
more on the paper
2010-03-26, by Christian Urban
simplification
2010-03-26, by Christian Urban
merge
2010-03-26, by Cezary Kaliszyk
Describe 'nominal_datatype2'.
2010-03-26, by Cezary Kaliszyk
Fixed renamings.
2010-03-26, by Cezary Kaliszyk
merged
2010-03-26, by Christian Urban
Removed remaining cheats + some cleaning.
2010-03-26, by Cezary Kaliszyk
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
2010-03-26, by Cezary Kaliszyk
Update cheats in TODO.
2010-03-26, by Cezary Kaliszyk
Removed another cheat and cleaned the code a bit.
2010-03-26, by Cezary Kaliszyk
Fix Manual/LamEx for experiments.
2010-03-26, by Cezary Kaliszyk
Proper bn_rsp, for bn functions calling each other.
2010-03-25, by Cezary Kaliszyk
Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-25, by Cezary Kaliszyk
Update TODO
2010-03-25, by Cezary Kaliszyk
Showed ACons_subst.
2010-03-25, by Cezary Kaliszyk
Only ACons_subst left to show.
2010-03-25, by Cezary Kaliszyk
Solved all boring subgoals, and looking at properly defning permute_bv
2010-03-25, by Cezary Kaliszyk
One more copy-and-paste in core-haskell.
2010-03-25, by Cezary Kaliszyk
Properly defined permute_bn. No more sorry's in Let strong induction.
2010-03-25, by Cezary Kaliszyk
Showed Let substitution.
2010-03-25, by Cezary Kaliszyk
Only let substitution is left.
2010-03-25, by Cezary Kaliszyk
further in the proof
2010-03-25, by Cezary Kaliszyk
trying to prove the string induction for let.
2010-03-25, by Cezary Kaliszyk
added experiemental permute_bn
2010-03-25, by Christian Urban
first attempt of strong induction for lets with assignments
2010-03-25, by Christian Urban
more on the paper
2010-03-25, by Christian Urban
more on the paper
2010-03-24, by Christian Urban
Further in the strong induction proof.
2010-03-24, by Cezary Kaliszyk
Solved one of the strong-induction goals.
2010-03-24, by Cezary Kaliszyk
avoiding for atom.
2010-03-24, by Cezary Kaliszyk
Started proving strong induction.
2010-03-24, by Cezary Kaliszyk
stating the strong induction; further.
2010-03-24, by Cezary Kaliszyk
Working on stating induct.
2010-03-24, by Cezary Kaliszyk
some tuning; possible fix for strange paper generation
2010-03-24, by Christian Urban
more on the paper
2010-03-24, by Christian Urban
merge
2010-03-24, by Cezary Kaliszyk
Showed support of Core Haskell
2010-03-24, by Cezary Kaliszyk
Support proof modification for Core Haskell.
2010-03-24, by Cezary Kaliszyk
Experiments with Core Haskell support.
2010-03-24, by Cezary Kaliszyk
Export all the cheats needed for Core Haskell.
2010-03-24, by Cezary Kaliszyk
Compute Fv for non-recursive bn functions calling other bn functions
2010-03-24, by Cezary Kaliszyk
Core Haskell experiments.
2010-03-24, by Cezary Kaliszyk
tuned paper
2010-03-24, by Christian Urban
more of the paper
2010-03-23, by Christian Urban
merged
2010-03-23, by Christian Urban
more tuning in the paper
2010-03-23, by Christian Urban
merge
2010-03-23, by Cezary Kaliszyk
Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
2010-03-23, by Cezary Kaliszyk
merged
2010-03-23, by Christian Urban
more tuning
2010-03-23, by Christian Urban
tuned paper
2010-03-23, by Christian Urban
more on the paper
2010-03-23, by Christian Urban
merge
2010-03-23, by Cezary Kaliszyk
Modification to Core Haskell to make it accepted with an empty binding function.
2010-03-23, by Cezary Kaliszyk
merged
2010-03-23, by Christian Urban
tuned paper
2010-03-23, by Christian Urban
Initial list unfoldings in Core Haskell.
2010-03-23, by Cezary Kaliszyk
compiles
2010-03-23, by Cezary Kaliszyk
More modification needed for compilation
2010-03-23, by Cezary Kaliszyk
Moved let properties from Term5 to ExLetRec.
2010-03-23, by Cezary Kaliszyk
Move Let properties to ExLet
2010-03-23, by Cezary Kaliszyk
Added missing file
2010-03-23, by Cezary Kaliszyk
More reorganization.
2010-03-23, by Cezary Kaliszyk
Move Leroy out of Test, rename accordingly.
2010-03-23, by Cezary Kaliszyk
Term1 is identical to Example 3
2010-03-23, by Cezary Kaliszyk
Move example3 out.
2010-03-23, by Cezary Kaliszyk
Move Ex1 and Ex2 out of Test
2010-03-23, by Cezary Kaliszyk
Move examples which create more permutations out
2010-03-23, by Cezary Kaliszyk
Move LamEx out of Test.
2010-03-23, by Cezary Kaliszyk
Move lambda examples to manual
2010-03-23, by Cezary Kaliszyk
Move manual examples to a subdirectory.
2010-03-23, by Cezary Kaliszyk
Removed compat tests.
2010-03-23, by Cezary Kaliszyk
merge
2010-03-23, by Cezary Kaliszyk
Move Non-respectful examples to NotRsp
2010-03-23, by Cezary Kaliszyk
merged
2010-03-23, by Christian Urban
more on the paper
2010-03-23, by Christian Urban
Move the comment to appropriate place.
2010-03-23, by Cezary Kaliszyk
Remove compose_eqvt
2010-03-23, by Cezary Kaliszyk
sym proof with compose.
2010-03-22, by Cezary Kaliszyk
Marked the place where a compose lemma applies.
2010-03-22, by Cezary Kaliszyk
merge
2010-03-22, by Cezary Kaliszyk
equivp_cheat can be removed for all one-permutation examples.
2010-03-22, by Cezary Kaliszyk
merged
2010-03-22, by Christian Urban
more on the paper
2010-03-22, by Christian Urban
merged
2010-03-22, by Christian Urban
tuned paper
2010-03-22, by Christian Urban
Got rid of alpha_bn_rsp_cheat.
2010-03-22, by Cezary Kaliszyk
alpha_bn_rsp_pre automatized.
2010-03-22, by Cezary Kaliszyk
merge
2010-03-22, by Cezary Kaliszyk
fv_rsp proved automatically.
2010-03-22, by Cezary Kaliszyk
more on the paper
2010-03-22, by Christian Urban
merged
2010-03-22, by Christian Urban
tuned paper
2010-03-22, by Christian Urban
some tuning
2010-03-22, by Christian Urban
Strong induction for Type Schemes.
2010-03-22, by Cezary Kaliszyk
Fixed missing colon.
2010-03-22, by Cezary Kaliszyk
tuned paper
2010-03-21, by Christian Urban
merged
2010-03-20, by Christian Urban
proved at_set_avoiding2 which is needed for strong induction principles
2010-03-20, by Christian Urban
moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
2010-03-20, by Christian Urban
Size experiments.
2010-03-20, by Cezary Kaliszyk
Use 'alpha_bn_refl' to get rid of one of the sorrys.
2010-03-20, by Cezary Kaliszyk
Build alpha-->alphabn implications
2010-03-20, by Cezary Kaliszyk
Prove reflp for all relations.
2010-03-20, by Cezary Kaliszyk
started cleaning up and introduced 3 versions of ~~gen
2010-03-20, by Christian Urban
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
2010-03-20, by Christian Urban
more work on the paper
2010-03-19, by Christian Urban
less
more
|
(0)
-1000
-120
+120
+1000
tip