Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
Wed, 17 Mar 2010 17:40:14 +0100 Cezary Kaliszyk Proper compose_sym2 changeset | files
Wed, 17 Mar 2010 17:11:23 +0100 Christian Urban merged changeset | files
Wed, 17 Mar 2010 17:10:19 +0100 Christian Urban temporarily disabled tests in Nominal/ROOT changeset | files
Wed, 17 Mar 2010 15:13:31 +0100 Christian Urban made paper to compile changeset | files
Wed, 17 Mar 2010 15:13:03 +0100 Christian Urban added partial proof for the strong induction principle changeset | files
Wed, 17 Mar 2010 17:09:01 +0100 Cezary Kaliszyk Trying to find a compose lemma for 2 arguments. changeset | files
Wed, 17 Mar 2010 12:23:04 +0100 Cezary Kaliszyk merge changeset | files
Wed, 17 Mar 2010 12:18:35 +0100 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages. changeset | files
Wed, 17 Mar 2010 11:54:22 +0100 Christian Urban merged changeset | files
Wed, 17 Mar 2010 11:53:56 +0100 Christian Urban added proof of supp/fv for type schemes changeset | files
Wed, 17 Mar 2010 11:40:58 +0100 Cezary Kaliszyk Updated Type Schemes to automatic lifting. One goal is not true because of the restriction. changeset | files
Wed, 17 Mar 2010 11:20:24 +0100 Cezary Kaliszyk Remove Term5a, since it is now identical to Term5. changeset | files
Wed, 17 Mar 2010 11:11:42 +0100 Cezary Kaliszyk merge changeset | files
Wed, 17 Mar 2010 11:11:25 +0100 Cezary Kaliszyk Finished all proofs in Term5 and Term5n. changeset | files
Wed, 17 Mar 2010 10:34:25 +0100 Christian Urban added partial proof of supp for type schemes changeset | files
Wed, 17 Mar 2010 09:57:54 +0100 Cezary Kaliszyk Fix in alpha; support of the recursive Let works :) changeset | files
Wed, 17 Mar 2010 09:42:56 +0100 Cezary Kaliszyk The recursive supp just has one equation too much. changeset | files
Wed, 17 Mar 2010 09:25:01 +0100 Cezary Kaliszyk Fix for the change of alpha_gen. changeset | files
Wed, 17 Mar 2010 09:18:27 +0100 Cezary Kaliszyk merge changeset | files
Wed, 17 Mar 2010 09:17:55 +0100 Cezary Kaliszyk Generate compound FV and Alpha for recursive bindings. changeset | files
Wed, 17 Mar 2010 08:39:46 +0100 Cezary Kaliszyk Lifting theorems with compound fv and compound alpha. changeset | files
Wed, 17 Mar 2010 08:07:25 +0100 Christian Urban commented out examples that should not work; but for example type-scheme example should work changeset | files
Wed, 17 Mar 2010 06:49:33 +0100 Christian Urban added another supp-proof for the non-recursive case changeset | files
Tue, 16 Mar 2010 20:07:13 +0100 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not. changeset | files
Tue, 16 Mar 2010 18:19:00 +0100 Cezary Kaliszyk merge changeset | files
Tue, 16 Mar 2010 18:18:08 +0100 Cezary Kaliszyk The old recursive alpha works fine. changeset | files
Tue, 16 Mar 2010 18:13:34 +0100 Christian Urban added the final unfolded result changeset | files
Tue, 16 Mar 2010 18:02:08 +0100 Christian Urban merge and proof of support for non-recursive case changeset | files
Tue, 16 Mar 2010 17:20:46 +0100 Cezary Kaliszyk Added Term5 non-recursive. The bug is there only for the recursive case. changeset | files
Tue, 16 Mar 2010 17:11:32 +0100 Cezary Kaliszyk Alpha is wrong. changeset | files
Tue, 16 Mar 2010 16:51:06 +0100 Cezary Kaliszyk alpha_bn doesn't need the permutation in non-recursive case. changeset | files
Tue, 16 Mar 2010 16:17:05 +0100 Cezary Kaliszyk alpha5_transp and equivp changeset | files
Tue, 16 Mar 2010 15:38:14 +0100 Cezary Kaliszyk alpha5_symp proved. changeset | files
Tue, 16 Mar 2010 15:27:47 +0100 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings. changeset | files
Tue, 16 Mar 2010 12:08:37 +0100 Cezary Kaliszyk The proof in 'Test' gets simpler. changeset | files
Tue, 16 Mar 2010 12:06:22 +0100 Cezary Kaliszyk Removed pi o bn = bn' assumption in alpha changeset | files
Mon, 15 Mar 2010 23:42:56 +0100 Christian Urban merged (confirmed to work with Isabelle from 6th March) changeset | files
Mon, 15 Mar 2010 17:52:31 +0100 Christian Urban another synchronisation changeset | files
Mon, 15 Mar 2010 17:51:35 +0100 Christian Urban proof for support when bn-function is present, but fb_function is empty changeset | files
Mon, 15 Mar 2010 17:42:17 +0100 Cezary Kaliszyk fv_eqvt_cheat no longer needed. changeset | files
Mon, 15 Mar 2010 14:32:05 +0100 Cezary Kaliszyk derive "inducts" from "induct" instead of lifting again is much faster. changeset | files
Mon, 15 Mar 2010 13:56:17 +0100 Cezary Kaliszyk build_eqvts works with recursive case if proper induction rule is used. changeset | files
Mon, 15 Mar 2010 11:50:12 +0100 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work. changeset | files
Mon, 15 Mar 2010 10:36:09 +0100 Cezary Kaliszyk LF works with new alpha...? changeset | files
Mon, 15 Mar 2010 10:07:15 +0100 Cezary Kaliszyk explicit flag "cheat_equivp" changeset | files
Mon, 15 Mar 2010 10:02:19 +0100 Cezary Kaliszyk Prove alpha_gen_compose_eqvt changeset | files
Mon, 15 Mar 2010 09:27:25 +0100 Cezary Kaliszyk Use eqvt. changeset | files
Mon, 15 Mar 2010 08:39:23 +0100 Christian Urban added preliminary test version....but Test works now changeset | files
Mon, 15 Mar 2010 08:28:10 +0100 Christian Urban added an eqvt-proof for bi changeset | files
Mon, 15 Mar 2010 06:11:35 +0100 Christian Urban synchronised with main hg-repository; used add_typedef_global in nominal_atoms changeset | files
Sun, 14 Mar 2010 11:36:15 +0100 Christian Urban localised the typedef in Attic (requires new Isabelle) changeset | files
Sat, 13 Mar 2010 13:49:15 +0100 Christian Urban started supp-fv proofs (is going to work) changeset | files
Fri, 12 Mar 2010 17:42:31 +0100 Cezary Kaliszyk Even with pattern simplified to a single clause, the supp equation doesn't seem true. changeset | files
Fri, 12 Mar 2010 12:42:35 +0100 Cezary Kaliszyk Still don't know how to prove supp=fv for simplest Let... changeset | files
Thu, 11 Mar 2010 20:49:31 +0100 Cezary Kaliszyk Do not fail if the finite support proof fails. changeset | files
Thu, 11 Mar 2010 19:43:50 +0100 Christian Urban generalised the supp for atoms to all concrete atoms (not just names) changeset | files
Thu, 11 Mar 2010 19:41:11 +0100 Christian Urban support of atoms at the end of Abs.thy changeset | files
Thu, 11 Mar 2010 19:24:07 +0100 Cezary Kaliszyk Trying to prove atom_image_fresh_swap changeset | files
Thu, 11 Mar 2010 17:49:07 +0100 Cezary Kaliszyk Finite_support proof no longer needed in LF. changeset | files
Thu, 11 Mar 2010 17:47:29 +0100 Cezary Kaliszyk Show that the new types are in finite support typeclass. changeset | files
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip
nominal2