https://cflmark.nms.kcl.ac.uk/hg/nominal2/ en-us nominal2: FIXME-TODO history FIXME-TODO revision history Added Brian's suggestion. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/7e9e96158025/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Mon, 22 Feb 2010 10:16:13 +0100 Update TODO https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/c093b2e6e9ae/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Mon, 22 Feb 2010 09:55:43 +0100 More indentation, names and todo cleaning in the quotient package https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/551eacf071d7/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Tue, 09 Feb 2010 15:28:15 +0100 use of equiv_relation_chk in quotient_term https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/9c3b3eaecaff/FIXME-TODO Christian Urban <urbanc@in.tum.de> Wed, 27 Jan 2010 08:41:42 +0100 properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/dae038c8cd69/FIXME-TODO Christian Urban <urbanc@in.tum.de> Mon, 25 Jan 2010 18:52:22 +0100 cleaned some theorems https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/c46b6abad24b/FIXME-TODO Christian Urban <urbanc@in.tum.de> Mon, 25 Jan 2010 17:53:08 +0100 Lifted Peter's Sigma lemma with Ex1. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/aa960d16570f/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Thu, 21 Jan 2010 12:50:43 +0100 one more item in the list of Markus https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/f537d570fff8/FIXME-TODO Christian Urban <urbanc@in.tum.de> Wed, 13 Jan 2010 16:39:20 +0100 added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML) https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/f0a78fda343f/FIXME-TODO Christian Urban <urbanc@in.tum.de> Sat, 26 Dec 2009 20:45:37 +0100 added "Highest Priority" category; and tuned slightly code https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/54f186bb5e3e/FIXME-TODO Christian Urban <urbanc@in.tum.de> Tue, 22 Dec 2009 22:10:48 +0100 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 https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/e9e205b904e2/FIXME-TODO Christian Urban <urbanc@in.tum.de> Mon, 21 Dec 2009 22:36:31 +0100 various tunings; map_lookup now raises an exception; addition to FIXME-TODO https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/c1989de100b4/FIXME-TODO Christian Urban <urbanc@in.tum.de> Sat, 19 Dec 2009 22:04:34 +0100 Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/544b05e03ec0/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Wed, 16 Dec 2009 12:15:41 +0100 FIXME/TODO. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/5ef8be0175f6/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Mon, 14 Dec 2009 13:56:24 +0100 FSet3 minor fixes + cases https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/1e08743b6997/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 11 Dec 2009 16:32:40 +0100 Updated TODO list together. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/54cb69112477/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 11 Dec 2009 13:51:08 +0100 added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/91b079db7380/FIXME-TODO Christian Urban <urbanc@in.tum.de> Thu, 10 Dec 2009 18:28:30 +0100 More name changes https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/6348c2a57ec2/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 04 Dec 2009 15:18:33 +0100 code cleaning and renaming https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/9b1ad366827f/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 04 Dec 2009 14:35:36 +0100 Removed previous inj_repabs_tac https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/3f657c4fbefa/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 04 Dec 2009 14:11:03 +0100 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/6b77cfd508e9/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 04 Dec 2009 12:20:49 +0100 Fixes after big merge. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/b00a9b58264d/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 04 Dec 2009 09:33:32 +0100 The big merge; probably non-functional. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/6b3be083229c/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 04 Dec 2009 09:25:27 +0100 First version of the deterministic rep-abs-inj-tac. https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/8c7597b19f0e/FIXME-TODO Cezary Kaliszyk <kaliszyk@in.tum.de> Fri, 04 Dec 2009 09:01:13 +0100 removed quot argument...not all examples work anymore https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/91c374abde06/FIXME-TODO Christian Urban <urbanc@in.tum.de> Thu, 03 Dec 2009 15:03:31 +0100 first version of internalised quotient theorems; added FIXME-TODO https://cflmark.nms.kcl.ac.uk/hg/nominal2/log/d2c9a72e52e0/FIXME-TODO Christian Urban <urbanc@in.tum.de> Thu, 03 Dec 2009 13:59:53 +0100