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/QuotMain.thy
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 01:03:34 +0100 Christian Urban tuned previous commit further 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
Fri, 08 Jan 2010 10:39:08 +0100 Cezary Kaliszyk Modifictaions for new_relation. file | diff | annotate
Fri, 25 Dec 2009 00:58:06 +0100 Christian Urban tuned file | diff | annotate
Wed, 23 Dec 2009 13:45:42 +0100 Christian Urban renamed QUOT_TYPE to Quot_Type 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
Tue, 22 Dec 2009 20:51:37 +0100 Christian Urban tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works 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
Thu, 17 Dec 2009 17:59:12 +0100 Christian Urban minor cleaning file | diff | annotate
Thu, 17 Dec 2009 14:58:33 +0100 Christian Urban moved the QuotMain code into two ML-files file | diff | annotate
Tue, 15 Dec 2009 16:40:00 +0100 Cezary Kaliszyk lambda_prs & solve_quotient_assum cleaned. file | diff | annotate
Tue, 15 Dec 2009 15:38:17 +0100 Christian Urban some commenting file | diff | annotate
Mon, 14 Dec 2009 14:24:08 +0100 Cezary Kaliszyk Fixed previous commit. file | diff | annotate
Mon, 14 Dec 2009 13:58:51 +0100 Cezary Kaliszyk Moved DETERM inside Repeat & added SOLVE around quotient_tac. file | diff | annotate
Mon, 14 Dec 2009 10:19:27 +0100 Cezary Kaliszyk reply to question in code file | diff | annotate
Mon, 14 Dec 2009 10:12:23 +0100 Cezary Kaliszyk Reply in code. file | diff | annotate
Sun, 13 Dec 2009 02:47:47 +0100 Christian Urban a few code annotations file | diff | annotate
Sun, 13 Dec 2009 02:35:34 +0100 Christian Urban another pass on apply_rsp file | diff | annotate
Sun, 13 Dec 2009 01:56:19 +0100 Christian Urban managed to simplify apply_rsp file | diff | annotate
Sat, 12 Dec 2009 18:43:42 +0100 Christian Urban tried to simplify apply_rsp_tac; failed at the moment; added some questions file | diff | annotate
Sat, 12 Dec 2009 18:01:22 +0100 Christian Urban some trivial changes file | diff | annotate
Sat, 12 Dec 2009 16:40:29 +0100 Christian Urban trivial cleaning of make_inst file | diff | annotate
Sat, 12 Dec 2009 15:23:58 +0100 Christian Urban tried to improve test; but fails file | diff | annotate
Sat, 12 Dec 2009 15:08:25 +0100 Christian Urban merged file | diff | annotate
Sat, 12 Dec 2009 15:07:59 +0100 Christian Urban annotated some questions to the code; some simple changes file | diff | annotate
Sat, 12 Dec 2009 14:57:34 +0100 Cezary Kaliszyk Answering the question in code. file | diff | annotate
Sat, 12 Dec 2009 02:01:33 +0100 Christian Urban tuned code file | diff | annotate
Sat, 12 Dec 2009 01:44:56 +0100 Christian Urban renamed quotient.ML to quotient_typ.ML file | diff | annotate
Fri, 11 Dec 2009 17:22:26 +0100 Cezary Kaliszyk Merge + Added LarryInt & Fset3 to tests. file | diff | annotate
Fri, 11 Dec 2009 17:19:38 +0100 Cezary Kaliszyk Renaming file | diff | annotate
Fri, 11 Dec 2009 17:03:34 +0100 Christian Urban deleted struct_match by Pattern.match (fixes a problem in LarryInt) file | diff | annotate
Fri, 11 Dec 2009 15:58:15 +0100 Christian Urban added Int example from Larry file | diff | annotate
Fri, 11 Dec 2009 08:28:41 +0100 Christian Urban changed error message file | diff | annotate
Fri, 11 Dec 2009 06:58:31 +0100 Christian Urban reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case file | diff | annotate
Thu, 10 Dec 2009 16:56:03 +0100 Christian Urban added maps-printout and tuned some comments 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 10:36:05 +0100 Cezary Kaliszyk minor file | diff | annotate
Thu, 10 Dec 2009 10:21:51 +0100 Cezary Kaliszyk Moved Unused part of locale to Unused QuotMain. file | diff | annotate
Thu, 10 Dec 2009 05:11:53 +0100 Christian Urban more tuning file | diff | annotate
Thu, 10 Dec 2009 05:02:34 +0100 Christian Urban tuned file | diff | annotate
Thu, 10 Dec 2009 04:53:48 +0100 Christian Urban simplified the instantiation of QUOT_TRUE in procedure_tac file | diff | annotate
Thu, 10 Dec 2009 04:35:08 +0100 Christian Urban completed previous commit file | diff | annotate
Thu, 10 Dec 2009 04:34:24 +0100 Christian Urban deleted DT/NDT diagnostic code file | diff | annotate
Wed, 09 Dec 2009 17:05:33 +0100 Cezary Kaliszyk Code cleaning. file | diff | annotate
Wed, 09 Dec 2009 16:09:25 +0100 Christian Urban tuned 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:35:21 +0100 Christian Urban deleted make_inst3 file | diff | annotate
Wed, 09 Dec 2009 15:29:36 +0100 Christian Urban tuned file | diff | annotate
Wed, 09 Dec 2009 15:28:01 +0100 Christian Urban tuned file | diff | annotate
Wed, 09 Dec 2009 15:24:11 +0100 Christian Urban moved function and tuned comment file | diff | annotate
Wed, 09 Dec 2009 15:11:49 +0100 Christian Urban improved fun_map_conv file | diff | annotate
Wed, 09 Dec 2009 06:21:09 +0100 Cezary Kaliszyk Arbitrary number of fun_map_tacs. 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:54:46 +0100 Christian Urban tuned code 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 20:34:00 +0100 Christian Urban properly set up the prs_rules 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: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:36:01 +0100 Christian Urban merged 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 15:42:29 +0100 Cezary Kaliszyk make_inst3 file | diff | annotate
Tue, 08 Dec 2009 15:12:36 +0100 Cezary Kaliszyk trans2 replaced with equals_rsp_tac file | diff | annotate
Tue, 08 Dec 2009 13:00:36 +0100 Cezary Kaliszyk Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned 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 04:21:14 +0100 Christian Urban tuned file | diff | annotate
Tue, 08 Dec 2009 04:14:02 +0100 Christian Urban the lift_tac produces a warning message if one of the three automatic proofs fails file | diff | annotate
Tue, 08 Dec 2009 01:25:43 +0100 Christian Urban added a thm list for ids file | diff | annotate
Tue, 08 Dec 2009 01:00:21 +0100 Christian Urban removed a fixme: map_info is now checked 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: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:21:57 +0100 Cezary Kaliszyk Handling of errors in lambda_prs_conv. 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:00 +0100 Cezary Kaliszyk make_inst for lambda_prs where the second quotient is not identity. 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