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/IntEx.thy
Thu, 21 Jan 2010 12:03:47 +0100 Cezary Kaliszyk Automatic injection of Bexeq file | diff | annotate
Thu, 21 Jan 2010 11:11:22 +0100 Cezary Kaliszyk Automatic cleaning of Bexeq<->Ex1 theorems. file | diff | annotate
Thu, 21 Jan 2010 10:55:09 +0100 Cezary Kaliszyk Using Bexeq_rsp, and manually lifted lemma with Ex1. file | diff | annotate
Thu, 21 Jan 2010 09:55:05 +0100 Cezary Kaliszyk Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles. file | diff | annotate
Thu, 14 Jan 2010 15:25:24 +0100 Cezary Kaliszyk Simplified matches_typ. file | diff | annotate
Wed, 13 Jan 2010 13:12:04 +0100 Cezary Kaliszyk Removed the 'oops' in IntEx. file | diff | annotate
Wed, 13 Jan 2010 00:46:31 +0100 Christian Urban tuned file | diff | annotate
Wed, 13 Jan 2010 00:45:28 +0100 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM" file | diff | annotate
Mon, 11 Jan 2010 11:51:19 +0100 Cezary Kaliszyk Fix for testing matching constants in regularize. file | diff | annotate
Mon, 11 Jan 2010 00:31:29 +0100 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM" 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
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
Sun, 20 Dec 2009 00:14:46 +0100 Christian Urban with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place file | diff | annotate
Sat, 19 Dec 2009 22:21:51 +0100 Christian Urban avoided global "open"s - replaced by local "open"s 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 08:55:30 +0100 Cezary Kaliszyk Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order. 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 05:59:49 +0100 Cezary Kaliszyk Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work. 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 22:24:24 +0100 Christian Urban decoupled QuotProd from QuotMain and also started new cleaning strategy file | diff | annotate
Tue, 08 Dec 2009 22:02:14 +0100 Christian Urban proper formulation of all preservation theorems file | diff | annotate
Tue, 08 Dec 2009 17:33:51 +0100 Christian Urban chnaged syntax to "lifting theorem" 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:35:40 +0100 Christian Urban added methods for the lifting_tac and the other tacs file | diff | annotate
Tue, 08 Dec 2009 13:01:23 +0100 Cezary Kaliszyk Another lambda example theorem proved. Seems it starts working properly. file | diff | annotate
Tue, 08 Dec 2009 12:36:28 +0100 Cezary Kaliszyk Nitpick found a counterexample for one lemma. file | diff | annotate
Tue, 08 Dec 2009 11:59:16 +0100 Cezary Kaliszyk Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples. file | diff | annotate
Tue, 08 Dec 2009 11:38:58 +0100 Cezary Kaliszyk It also regularizes. file | diff | annotate
Tue, 08 Dec 2009 11:28:04 +0100 Cezary Kaliszyk inj_repabs also works. file | diff | annotate
Tue, 08 Dec 2009 11:20:01 +0100 Cezary Kaliszyk merge file | diff | annotate
Tue, 08 Dec 2009 11:17:56 +0100 Cezary Kaliszyk An example of working cleaning for lambda lifting. Still not sure why Babs helps. file | diff | annotate
Mon, 07 Dec 2009 23:45:51 +0100 Christian Urban tuning of the code 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 18:49:14 +0100 Christian Urban clarified the function examples file | diff | annotate
Mon, 07 Dec 2009 17:57:33 +0100 Christian Urban first attempt to deal with Babs in regularise and cleaning (not yet working) file | diff | annotate
Mon, 07 Dec 2009 15:18:44 +0100 Cezary Kaliszyk merge file | diff | annotate
Mon, 07 Dec 2009 15:18:00 +0100 Cezary Kaliszyk make_inst for lambda_prs where the second quotient is not identity. file | diff | annotate
Mon, 07 Dec 2009 14:37:10 +0100 Christian Urban added "end" to each example theory 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
less more (0) tip
nominal2