Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FSet.thy
Fri, 30 Oct 2009 19:03:53 +0100 Cezary Kaliszyk Regularize for equalities and a better tactic. "alpha.cases" now lifts. file | diff | annotate
Fri, 30 Oct 2009 18:31:06 +0100 Cezary Kaliszyk Regularization file | diff | annotate
Fri, 30 Oct 2009 16:24:07 +0100 Cezary Kaliszyk Finally merged the code of the versions of regularize and tested examples. file | diff | annotate
Fri, 30 Oct 2009 15:30:33 +0100 Christian Urban not sure what changed here file | diff | annotate
Fri, 30 Oct 2009 14:25:37 +0100 Cezary Kaliszyk Finding applications and duplicates filtered out in abstractions file | diff | annotate
Fri, 30 Oct 2009 11:25:29 +0100 Cezary Kaliszyk Cleaning of the interface to lift. file | diff | annotate
Thu, 29 Oct 2009 08:06:49 +0100 Cezary Kaliszyk Fixed wrong CARD definition and removed the "Does not work anymore" comment. file | diff | annotate
Thu, 29 Oct 2009 07:29:12 +0100 Christian Urban merged file | diff | annotate
Wed, 28 Oct 2009 20:01:20 +0100 Christian Urban updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!) file | diff | annotate
Wed, 28 Oct 2009 18:08:38 +0100 Cezary Kaliszyk disambiguate ===> syntax file | diff | annotate
Wed, 28 Oct 2009 17:17:21 +0100 Cezary Kaliszyk cleaned FSet file | diff | annotate
Wed, 28 Oct 2009 16:48:57 +0100 Cezary Kaliszyk Some cleaning file | diff | annotate
Wed, 28 Oct 2009 16:05:59 +0100 Cezary Kaliszyk Fixes file | diff | annotate
Wed, 28 Oct 2009 15:25:36 +0100 Christian Urban merged file | diff | annotate
Wed, 28 Oct 2009 15:25:11 +0100 Christian Urban added infrastructure for defining lifted constants file | diff | annotate
Wed, 28 Oct 2009 12:22:06 +0100 Cezary Kaliszyk Fixed mistake in const generation, will postpone this. file | diff | annotate
Wed, 28 Oct 2009 10:29:00 +0100 Cezary Kaliszyk More finshed proofs and cleaning file | diff | annotate
Wed, 28 Oct 2009 10:17:07 +0100 Cezary Kaliszyk Proof of append_rsp file | diff | annotate
Wed, 28 Oct 2009 01:49:31 +0100 Christian Urban merged file | diff | annotate
Wed, 28 Oct 2009 01:48:45 +0100 Christian Urban added a function for matching types file | diff | annotate
Tue, 27 Oct 2009 18:05:45 +0100 Cezary Kaliszyk Manual conversion of equality to equivalence allows lifting append_assoc. file | diff | annotate
Tue, 27 Oct 2009 18:02:35 +0100 Cezary Kaliszyk Simplfied interface to repabs_injection. file | diff | annotate
Tue, 27 Oct 2009 17:08:47 +0100 Cezary Kaliszyk map_append lifted automatically. file | diff | annotate
Tue, 27 Oct 2009 16:15:56 +0100 Cezary Kaliszyk Manually lifted Map_Append. file | diff | annotate
Tue, 27 Oct 2009 14:59:00 +0100 Cezary Kaliszyk Fixed APPLY_RSP vs Cong in the InjRepAbs tactic. file | diff | annotate
Tue, 27 Oct 2009 12:20:57 +0100 Cezary Kaliszyk Simplifying FSet with new functions. file | diff | annotate
Mon, 26 Oct 2009 15:31:53 +0100 Cezary Kaliszyk Simplifying Int and Working on map file | diff | annotate
Mon, 26 Oct 2009 11:55:36 +0100 Cezary Kaliszyk Finished the code for adding lower defs, and more things moved to QuotMain file | diff | annotate
Mon, 26 Oct 2009 11:34:02 +0100 Cezary Kaliszyk Making all the definitions from the original ones file | diff | annotate
Mon, 26 Oct 2009 10:02:50 +0100 Cezary Kaliszyk Cleaning and fixing. file | diff | annotate
Sun, 25 Oct 2009 01:15:03 +0200 Christian Urban proved the two lemmas in QuotScript (reformulated them without leading forall) file | diff | annotate
Sat, 24 Oct 2009 18:17:38 +0200 Christian Urban changed the definitions of liftet constants to use fun_maps file | diff | annotate
Sat, 24 Oct 2009 17:29:27 +0200 Cezary Kaliszyk Finally lifted induction, with some manually added simplification lemmas. file | diff | annotate
Sat, 24 Oct 2009 16:15:33 +0200 cek Merge file | diff | annotate
Sat, 24 Oct 2009 16:15:58 +0200 Cezary Kaliszyk Preparing infrastructire for LAMBDA_PRS file | diff | annotate
Sat, 24 Oct 2009 16:09:05 +0200 Christian Urban moved the map_funs setup into QuotMain file | diff | annotate
Sat, 24 Oct 2009 14:00:18 +0200 Cezary Kaliszyk Finally completely lift the previously lifted theorems + clean some old stuff file | diff | annotate
Sat, 24 Oct 2009 13:00:54 +0200 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before file | diff | annotate
Sat, 24 Oct 2009 10:16:53 +0200 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before file | diff | annotate
Sat, 24 Oct 2009 08:24:26 +0200 cek Cleaning the mess file | diff | annotate
Sat, 24 Oct 2009 08:09:40 +0200 cek Merge file | diff | annotate
Sat, 24 Oct 2009 08:09:09 +0200 cek Better tactic and simplified the proof further file | diff | annotate
Sat, 24 Oct 2009 01:33:29 +0200 Christian Urban fixed problem with incorrect ABS/REP name file | diff | annotate
Fri, 23 Oct 2009 18:20:06 +0200 Cezary Kaliszyk Stronger tactic, simpler proof. file | diff | annotate
Fri, 23 Oct 2009 16:34:20 +0200 Cezary Kaliszyk Split Finite Set example into separate file file | diff | annotate
less more (0) tip
nominal2