Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Theory name changes for JEdit
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 24 Jun 2011 11:03:53 +0900
changeset 2895 65efa1c7563c
parent 2894 8ec94871de1e
child 2896 59be22e05a0a
Theory name changes for JEdit
Nominal/Ex/CPS/CPS1_Plotkin.thy file | annotate | diff | comparison | revisions
Nominal/Ex/CPS/CPS2_DanvyNielsen.thy file | annotate | diff | comparison | revisions
Nominal/Ex/CPS/CPS3_DanvyFilinski.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Fri Jun 24 10:54:31 2011 +0900
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Fri Jun 24 11:03:53 2011 +0900
@@ -1,5 +1,5 @@
 header {* CPS conversion *}
-theory Plotkin
+theory CPS1_Plotkin
 imports Lt
 begin
 
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Fri Jun 24 10:54:31 2011 +0900
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Fri Jun 24 11:03:53 2011 +0900
@@ -1,5 +1,5 @@
 header {* CPS transformation of Danvy and Nielsen *}
-theory DanvyNielsen
+theory CPS2_DanvyNielsen
 imports Lt
 begin
 
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Fri Jun 24 10:54:31 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Fri Jun 24 11:03:53 2011 +0900
@@ -1,5 +1,5 @@
 header {* CPS transformation of Danvy and Filinski *}
-theory DanvyFilinski imports Lt begin
+theory CPS3_DanvyFilinski imports Lt begin
 
 nominal_primrec
   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
nominal2