https://cflmark.nms.kcl.ac.uk/hg/regexp/ en-us regexp: IsaMakefile history IsaMakefile revision history for slides https://cflmark.nms.kcl.ac.uk/hg/regexp/log/79401279ba21/IsaMakefile urbanc Wed, 29 Aug 2012 13:05:46 +0000 partially updated conference paper; slightly tuned journal paper https://cflmark.nms.kcl.ac.uk/hg/regexp/log/d47c2143ab8a/IsaMakefile urbanc Wed, 22 Feb 2012 13:25:49 +0000 some polishing of the repository https://cflmark.nms.kcl.ac.uk/hg/regexp/log/813e7257c7c3/IsaMakefile urbanc Mon, 20 Feb 2012 11:02:50 +0000 added slides for a talk in St Andrews https://cflmark.nms.kcl.ac.uk/hg/regexp/log/1abf8586ee6b/IsaMakefile urbanc Sun, 20 Nov 2011 22:53:50 +0000 changes according to afp-submission https://cflmark.nms.kcl.ac.uk/hg/regexp/log/5d724fe0e096/IsaMakefile urbanc Mon, 22 Aug 2011 12:49:27 +0000 added directory for journal version; took uptodate version of the theory files https://cflmark.nms.kcl.ac.uk/hg/regexp/log/e93760534354/IsaMakefile urbanc Wed, 18 May 2011 19:54:43 +0000 added an option fullpaper to IsaMakefile https://cflmark.nms.kcl.ac.uk/hg/regexp/log/e5116c2e6187/IsaMakefile urbanc Mon, 07 Feb 2011 11:12:36 +0000 more on the introduction https://cflmark.nms.kcl.ac.uk/hg/regexp/log/828ea293b61f/IsaMakefile urbanc Fri, 04 Feb 2011 22:54:29 +0000 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts. https://cflmark.nms.kcl.ac.uk/hg/regexp/log/d94209ad2880/IsaMakefile zhang Thu, 03 Feb 2011 12:00:06 +0000 a little bit in the introduction https://cflmark.nms.kcl.ac.uk/hg/regexp/log/0d4d5bb321dc/IsaMakefile urbanc Wed, 02 Feb 2011 13:54:07 +0000 Myhill.thy IsabelleMakefile modified https://cflmark.nms.kcl.ac.uk/hg/regexp/log/d71424eb5d0c/IsaMakefile zhang Mon, 31 Jan 2011 14:51:47 +0000 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP https://cflmark.nms.kcl.ac.uk/hg/regexp/log/f5cc33a0ba99/IsaMakefile wu Wed, 26 Jan 2011 22:51:51 +0000 1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML https://cflmark.nms.kcl.ac.uk/hg/regexp/log/b6815473ee2e/IsaMakefile zhang Tue, 25 Jan 2011 12:14:31 +0000 Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. https://cflmark.nms.kcl.ac.uk/hg/regexp/log/f5db9e08effc/IsaMakefile zhang Mon, 24 Jan 2011 11:29:55 +0000 added paper https://cflmark.nms.kcl.ac.uk/hg/regexp/log/f72c82bf59e5/IsaMakefile urbanc Thu, 25 Nov 2010 18:54:45 +0000 added initial slides for informal talk in Cambridge https://cflmark.nms.kcl.ac.uk/hg/regexp/log/663816814e3e/IsaMakefile urbanc Wed, 03 Nov 2010 21:42:44 +0000