2010-04-01 Cezary Kaliszyk fv_perm_bn
2010-04-01 Cezary Kaliszyk Minor formula fixes.
2010-04-01 Christian Urban fixed alpha_bn
2010-04-01 Christian Urban current state
2010-04-01 Christian Urban merged
2010-04-01 Christian Urban added alpha_bn definition
2010-04-01 Cezary Kaliszyk hfill for right aligning single table cells.
2010-04-01 Cezary Kaliszyk Cleaning the strong induction example.
2010-04-01 Cezary Kaliszyk minor
2010-04-01 Cezary Kaliszyk Fighting with space in displaying strong induction...
2010-04-01 Cezary Kaliszyk starting strong induction
2010-04-01 Cezary Kaliszyk General paper minor fixes.
2010-04-01 Cezary Kaliszyk Forgot to save before commit.
2010-04-01 Cezary Kaliszyk Let with multiple bindings.
2010-04-01 Cezary Kaliszyk Fill the space below the figure.
2010-04-01 Christian Urban last commit for now.
2010-04-01 Christian Urban more on the conclusion
2010-04-01 Christian Urban completed related work section
2010-04-01 Christian Urban more on the paper
2010-03-31 Christian Urban added an item about alpha-equivalence (the existential should be closer to the abstraction)
2010-03-31 Christian Urban polished everything up to TODO
2010-03-31 Christian Urban merged
2010-03-31 Christian Urban added alpha-definition for ~~ty
2010-03-31 Cezary Kaliszyk permute_bn
2010-03-31 Christian Urban abbreviations for \<otimes> and \<oplus>
2010-03-31 Christian Urban merged
2010-03-31 Christian Urban a test with let having multiple bodies
2010-03-31 Christian Urban polished and removed tys from bn-functions.
2010-03-31 Cezary Kaliszyk merge
2010-03-31 Cezary Kaliszyk More on paper
2010-03-31 Christian Urban started to polish alpha-equivalence section, but needs more work
2010-03-31 Christian Urban started with a related work section
2010-03-30 Christian Urban polished and added an example for fvars
2010-03-30 Christian Urban cleaned up the section about fv's
2010-03-30 Christian Urban tuned beginning of section 4
2010-03-30 Cezary Kaliszyk More on section 5.
2010-03-30 Cezary Kaliszyk More on section 5.
2010-03-30 Christian Urban merged
2010-03-30 Christian Urban removed "raw" distinction
2010-03-30 Cezary Kaliszyk More on Section 5
2010-03-30 Cezary Kaliszyk Beginning of section 5.
2010-03-30 Christian Urban merged
2010-03-30 Cezary Kaliszyk Avoid mentioning other nominal datatypes as it makes things too complicated.
2010-03-30 Christian Urban merged
2010-03-30 Cezary Kaliszyk close the missing parenthesis on both sides.
2010-03-30 Christian Urban merged
2010-03-30 Christian Urban changes to section 2
2010-03-30 Cezary Kaliszyk Clean alpha
2010-03-30 Cezary Kaliszyk clean fv_bn
2010-03-30 Cezary Kaliszyk alpha_bn
2010-03-30 Cezary Kaliszyk Change @{text} to @{term}
2010-03-30 Cezary Kaliszyk alpha
2010-03-30 Cezary Kaliszyk more
2010-03-30 Cezary Kaliszyk fv and fv_bn
2010-03-30 Christian Urban more of the paper
2010-03-29 Christian Urban merged
2010-03-29 Cezary Kaliszyk Updated strong induction to modified definitions.
2010-03-29 Cezary Kaliszyk Initial renaming
2010-03-29 Christian Urban small changes in the core-haskell spec
2010-03-29 Cezary Kaliszyk Update according to paper
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk Changed to Lists.
2010-03-29 Christian Urban clarified core-haskell example
2010-03-29 Christian Urban spell check
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk Abs_gen and Abs_let simplifications.
2010-03-29 Christian Urban more on the paper
2010-03-28 Christian Urban fixed a problem due to a change in type-def (needs new Isabelle)
2010-03-28 Christian Urban merged
2010-03-28 Christian Urban more on the paper
2010-03-28 Christian Urban got rid of the aux-function on the raw level, by defining it with function on the quotient level
2010-03-27 Cezary Kaliszyk Lets finally abstract lists.
2010-03-27 Cezary Kaliszyk Core Haskell can now use proper strings.
2010-03-27 Cezary Kaliszyk Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
2010-03-27 Cezary Kaliszyk Remove list_eq notation.
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-27 Cezary Kaliszyk Equivariance when bn functions are lists.
2010-03-27 Cezary Kaliszyk Accepts lists in FV.
2010-03-27 Cezary Kaliszyk Parsing of list-bn functions into components.
2010-03-27 Cezary Kaliszyk Automatically compute support if only one type of Abs is present in the type.
2010-03-27 Cezary Kaliszyk Manually proved TySch support; All properties of TySch now true.
2010-03-27 Cezary Kaliszyk Generalize Abs_eq_iff.
2010-03-27 Cezary Kaliszyk Minor fix.
2010-03-27 Cezary Kaliszyk New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
2010-03-27 Cezary Kaliszyk Initial proof modifications for alpha_res
2010-03-27 Cezary Kaliszyk merge
2010-03-27 Cezary Kaliszyk Fv/Alpha now takes into account Alpha_Type given from the parser.
2010-03-27 Cezary Kaliszyk Minor cleaning.
2010-03-27 Christian Urban merged
2010-03-27 Christian Urban more on the paper
2010-03-27 Cezary Kaliszyk Removed some warnings.
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.
2010-03-26 Christian Urban merged
2010-03-26 Christian Urban more on the paper
2010-03-26 Christian Urban simplification
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Describe 'nominal_datatype2'.
2010-03-26 Cezary Kaliszyk Fixed renamings.
2010-03-26 Christian Urban merged
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
2010-03-26 Cezary Kaliszyk Update cheats in TODO.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
2010-03-26 Cezary Kaliszyk Fix Manual/LamEx for experiments.
2010-03-25 Cezary Kaliszyk Proper bn_rsp, for bn functions calling each other.
2010-03-25 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-25 Cezary Kaliszyk Update TODO
2010-03-25 Cezary Kaliszyk Showed ACons_subst.
2010-03-25 Cezary Kaliszyk Only ACons_subst left to show.
2010-03-25 Cezary Kaliszyk Solved all boring subgoals, and looking at properly defning permute_bv
2010-03-25 Cezary Kaliszyk One more copy-and-paste in core-haskell.
2010-03-25 Cezary Kaliszyk Properly defined permute_bn. No more sorry's in Let strong induction.
2010-03-25 Cezary Kaliszyk Showed Let substitution.
2010-03-25 Cezary Kaliszyk Only let substitution is left.
2010-03-25 Cezary Kaliszyk further in the proof
2010-03-25 Cezary Kaliszyk trying to prove the string induction for let.
2010-03-25 Christian Urban added experiemental permute_bn
2010-03-25 Christian Urban first attempt of strong induction for lets with assignments
(0) -1000 -120 +120 +1000 tip