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
2010-03-25 Christian Urban more on the paper
2010-03-24 Christian Urban more on the paper
2010-03-24 Cezary Kaliszyk Further in the strong induction proof.
2010-03-24 Cezary Kaliszyk Solved one of the strong-induction goals.
2010-03-24 Cezary Kaliszyk avoiding for atom.
2010-03-24 Cezary Kaliszyk Started proving strong induction.
2010-03-24 Cezary Kaliszyk stating the strong induction; further.
2010-03-24 Cezary Kaliszyk Working on stating induct.
2010-03-24 Christian Urban some tuning; possible fix for strange paper generation
2010-03-24 Christian Urban more on the paper
2010-03-24 Cezary Kaliszyk merge
2010-03-24 Cezary Kaliszyk Showed support of Core Haskell
2010-03-24 Cezary Kaliszyk Support proof modification for Core Haskell.
2010-03-24 Cezary Kaliszyk Experiments with Core Haskell support.
2010-03-24 Cezary Kaliszyk Export all the cheats needed for Core Haskell.
2010-03-24 Cezary Kaliszyk Compute Fv for non-recursive bn functions calling other bn functions
2010-03-24 Cezary Kaliszyk Core Haskell experiments.
2010-03-24 Christian Urban tuned paper
2010-03-23 Christian Urban more of the paper
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban more tuning in the paper
2010-03-23 Cezary Kaliszyk merge
2010-03-23 Cezary Kaliszyk Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban more tuning
2010-03-23 Christian Urban tuned paper
2010-03-23 Christian Urban more on the paper
2010-03-23 Cezary Kaliszyk merge
2010-03-23 Cezary Kaliszyk Modification to Core Haskell to make it accepted with an empty binding function.
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban tuned paper
2010-03-23 Cezary Kaliszyk Initial list unfoldings in Core Haskell.
2010-03-23 Cezary Kaliszyk compiles
2010-03-23 Cezary Kaliszyk More modification needed for compilation
2010-03-23 Cezary Kaliszyk Moved let properties from Term5 to ExLetRec.
2010-03-23 Cezary Kaliszyk Move Let properties to ExLet
2010-03-23 Cezary Kaliszyk Added missing file
2010-03-23 Cezary Kaliszyk More reorganization.
2010-03-23 Cezary Kaliszyk Move Leroy out of Test, rename accordingly.
2010-03-23 Cezary Kaliszyk Term1 is identical to Example 3
2010-03-23 Cezary Kaliszyk Move example3 out.
2010-03-23 Cezary Kaliszyk Move Ex1 and Ex2 out of Test
2010-03-23 Cezary Kaliszyk Move examples which create more permutations out
2010-03-23 Cezary Kaliszyk Move LamEx out of Test.
2010-03-23 Cezary Kaliszyk Move lambda examples to manual
2010-03-23 Cezary Kaliszyk Move manual examples to a subdirectory.
2010-03-23 Cezary Kaliszyk Removed compat tests.
2010-03-23 Cezary Kaliszyk merge
2010-03-23 Cezary Kaliszyk Move Non-respectful examples to NotRsp
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban more on the paper
2010-03-23 Cezary Kaliszyk Move the comment to appropriate place.
2010-03-23 Cezary Kaliszyk Remove compose_eqvt
2010-03-22 Cezary Kaliszyk sym proof with compose.
2010-03-22 Cezary Kaliszyk Marked the place where a compose lemma applies.
2010-03-22 Cezary Kaliszyk merge
2010-03-22 Cezary Kaliszyk equivp_cheat can be removed for all one-permutation examples.
2010-03-22 Christian Urban merged
2010-03-22 Christian Urban more on the paper
2010-03-22 Christian Urban merged
2010-03-22 Christian Urban tuned paper
2010-03-22 Cezary Kaliszyk Got rid of alpha_bn_rsp_cheat.
2010-03-22 Cezary Kaliszyk alpha_bn_rsp_pre automatized.
2010-03-22 Cezary Kaliszyk merge
2010-03-22 Cezary Kaliszyk fv_rsp proved automatically.
2010-03-22 Christian Urban more on the paper
2010-03-22 Christian Urban merged
2010-03-22 Christian Urban tuned paper
2010-03-22 Christian Urban some tuning
2010-03-22 Cezary Kaliszyk Strong induction for Type Schemes.
2010-03-22 Cezary Kaliszyk Fixed missing colon.
2010-03-21 Christian Urban tuned paper
2010-03-20 Christian Urban merged
2010-03-20 Christian Urban proved at_set_avoiding2 which is needed for strong induction principles
2010-03-20 Christian Urban moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
2010-03-20 Cezary Kaliszyk Size experiments.
2010-03-20 Cezary Kaliszyk Use 'alpha_bn_refl' to get rid of one of the sorrys.
2010-03-20 Cezary Kaliszyk Build alpha-->alphabn implications
2010-03-20 Cezary Kaliszyk Prove reflp for all relations.
2010-03-20 Christian Urban started cleaning up and introduced 3 versions of ~~gen
2010-03-20 Christian Urban moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
2010-03-19 Christian Urban more work on the paper
2010-03-19 Cezary Kaliszyk Described automatically created funs.
2010-03-19 Cezary Kaliszyk merge
2010-03-19 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
2010-03-19 Christian Urban picture
2010-03-19 Christian Urban merged
2010-03-19 Christian Urban polished
2010-03-19 Cezary Kaliszyk Update Test to use fset.
2010-03-19 Cezary Kaliszyk merge
2010-03-19 Cezary Kaliszyk Use fs typeclass in showing finite support + some cheat cleaning.
2010-03-19 Christian Urban merged
2010-03-19 Christian Urban more one the paper
2010-03-19 Cezary Kaliszyk Keep only one copy of infinite_Un.
2010-03-19 Cezary Kaliszyk Added a missing 'import'.
2010-03-19 Cezary Kaliszyk Showed the instance: fset::(at) fs
2010-03-19 Cezary Kaliszyk merge
2010-03-19 Cezary Kaliszyk Remove atom_decl from the parser.
2010-03-19 Cezary Kaliszyk TySch strong induction looks ok.
2010-03-19 Cezary Kaliszyk Working on TySch strong induction.
2010-03-19 Cezary Kaliszyk Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
2010-03-19 Christian Urban merged
2010-03-19 Christian Urban more tuning on the paper
2010-03-19 Cezary Kaliszyk The nominal infrastructure for fset. 'fs' missing, but not needed so far.
2010-03-19 Cezary Kaliszyk A few more theorems in FSet.
2010-03-18 Cezary Kaliszyk merge 2
2010-03-18 Cezary Kaliszyk merge 1
2010-03-18 Cezary Kaliszyk support of fset_to_set, support of fmap_atom.
2010-03-18 Christian Urban merged
2010-03-18 Christian Urban more tuning on the paper
2010-03-18 Christian Urban added item about size functions
(0) -1000 -120 +120 +1000 tip