https://cflmark.nms.kcl.ac.uk/hg/regexp/ en-us regexp: pres/IsaMakefile history pres/IsaMakefile revision history 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/pres/IsaMakefile zhang Thu, 03 Feb 2011 12:00:06 +0000 removed the inductive definition of Star and replaced it by a definition in terms of pow https://cflmark.nms.kcl.ac.uk/hg/regexp/log/b3898315e687/pres/IsaMakefile urbanc Wed, 02 Feb 2011 06:05:12 +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/pres/IsaMakefile zhang Mon, 24 Jan 2011 11:29:55 +0000