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.
Quot/Examples/FSet.thy
Tue, 26 Jan 2010 14:48:25 +0100 Cezary Kaliszyk 2 cases for regularize with split, lemmas with split now lift. file | diff | annotate
Tue, 26 Jan 2010 14:08:47 +0100 Cezary Kaliszyk Simpler statement that has the problem. file | diff | annotate
Tue, 26 Jan 2010 13:58:28 +0100 Cezary Kaliszyk Found a term that does not regularize. file | diff | annotate
Tue, 26 Jan 2010 13:53:56 +0100 Cezary Kaliszyk A triple is still ok. file | diff | annotate
Tue, 26 Jan 2010 13:38:42 +0100 Cezary Kaliszyk Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work. file | diff | annotate
Tue, 26 Jan 2010 09:54:43 +0100 Cezary Kaliszyk Generalized split_prs and split_rsp file | diff | annotate
Sun, 24 Jan 2010 23:41:27 +0100 Christian Urban test with splits file | diff | annotate
Thu, 24 Dec 2009 22:28:19 +0100 Christian Urban made the quotient_type definition more like typedef; now type variables need to be explicitly given file | diff | annotate
Wed, 23 Dec 2009 10:31:54 +0100 Christian Urban corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file file | diff | annotate
Tue, 22 Dec 2009 21:31:44 +0100 Christian Urban renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions file | diff | annotate
Tue, 22 Dec 2009 21:06:46 +0100 Christian Urban moved get_fun into quotient_term; this simplifies the overall including structure of the package file | diff | annotate
Mon, 21 Dec 2009 22:36:31 +0100 Christian Urban get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO file | diff | annotate
Sun, 20 Dec 2009 00:53:35 +0100 Christian Urban on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file file | diff | annotate
Sun, 20 Dec 2009 00:26:53 +0100 Christian Urban renamed "quotient" command to "quotient_type"; needs new keyword file to be installed file | diff | annotate
Thu, 17 Dec 2009 14:58:33 +0100 Christian Urban moved the QuotMain code into two ML-files file | diff | annotate
Fri, 11 Dec 2009 11:08:58 +0100 Cezary Kaliszyk New syntax for definitions. file | diff | annotate
Thu, 10 Dec 2009 12:25:12 +0100 Cezary Kaliszyk Regularized the hard lemma. file | diff | annotate
Thu, 10 Dec 2009 10:54:45 +0100 Cezary Kaliszyk Found the problem with ttt3. file | diff | annotate
Thu, 10 Dec 2009 04:23:13 +0100 Christian Urban moved the interpretation code into Unused.thy file | diff | annotate
Thu, 10 Dec 2009 03:47:10 +0100 Christian Urban removed memb and used standard mem (member from List.thy) file | diff | annotate
Thu, 10 Dec 2009 03:11:19 +0100 Christian Urban simplified proofs file | diff | annotate
Thu, 10 Dec 2009 02:46:08 +0100 Christian Urban removed quot_respect attribute of a non-standard lemma file | diff | annotate
Wed, 09 Dec 2009 15:59:02 +0100 Cezary Kaliszyk merge file | diff | annotate
Wed, 09 Dec 2009 15:57:47 +0100 Cezary Kaliszyk Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants. file | diff | annotate
Wed, 09 Dec 2009 15:11:49 +0100 Christian Urban improved fun_map_conv file | diff | annotate
Wed, 09 Dec 2009 05:59:49 +0100 Cezary Kaliszyk Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work. file | diff | annotate
Wed, 09 Dec 2009 00:03:18 +0100 Christian Urban tuned the examples and flagged the problematic cleaning lemmas in FSet file | diff | annotate
Tue, 08 Dec 2009 23:32:54 +0100 Christian Urban merged file | diff | annotate
Tue, 08 Dec 2009 23:30:47 +0100 Christian Urban implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges file | diff | annotate
Tue, 08 Dec 2009 23:04:25 +0100 Cezary Kaliszyk manually cleaned the hard lemma. file | diff | annotate
Tue, 08 Dec 2009 22:03:34 +0100 Cezary Kaliszyk An example which is hard to lift because of the interplay between lambda_prs and unfolding. file | diff | annotate
Tue, 08 Dec 2009 17:43:32 +0100 Christian Urban merged file | diff | annotate
Tue, 08 Dec 2009 17:40:58 +0100 Christian Urban added preserve rules to the cleaning_tac file | diff | annotate
Tue, 08 Dec 2009 17:39:34 +0100 Cezary Kaliszyk merge file | diff | annotate
Tue, 08 Dec 2009 17:35:04 +0100 Cezary Kaliszyk cleaning. file | diff | annotate
Tue, 08 Dec 2009 17:34:10 +0100 Christian Urban merged file | diff | annotate
Tue, 08 Dec 2009 17:30:00 +0100 Christian Urban changed names of attributes file | diff | annotate
Tue, 08 Dec 2009 16:56:37 +0100 Cezary Kaliszyk Manual regularization of a goal in FSet. file | diff | annotate
Tue, 08 Dec 2009 15:42:29 +0100 Cezary Kaliszyk make_inst3 file | diff | annotate
Tue, 08 Dec 2009 13:09:21 +0100 Cezary Kaliszyk Made fset work again to test all. file | diff | annotate
Tue, 08 Dec 2009 13:08:56 +0100 Cezary Kaliszyk Finished the proof of ttt2 and found bug in regularize when trying ttt3. file | diff | annotate
Mon, 07 Dec 2009 21:54:14 +0100 Christian Urban merged file | diff | annotate
Mon, 07 Dec 2009 21:53:50 +0100 Christian Urban removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===> file | diff | annotate
Mon, 07 Dec 2009 21:25:49 +0100 Cezary Kaliszyk 3 lambda examples in FSet. In the last one regularize_term fails. file | diff | annotate
Mon, 07 Dec 2009 14:35:45 +0100 Cezary Kaliszyk List moved after QuotMain file | diff | annotate
Mon, 07 Dec 2009 14:09:50 +0100 Christian Urban directory re-arrangement file | diff | annotate | base
less more (0) tip
nominal2