Added myself to the comments at the start of all files
authorSebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
Mon, 07 Jan 2019 13:44:19 +0100
changeset 292 293e9c6f22e1
parent 291 93db7414931d
child 293 8b55240e12c6
Added myself to the comments at the start of all files
thys/Abacus.thy
thys/Abacus_Defs.thy
thys/Abacus_Hoare.thy
thys/Abacus_Mopup.thy
thys/Rec_Def.thy
thys/Recursive.thy
thys/Turing.thy
thys/Turing_Hoare.thy
thys/UF.thy
thys/UTM.thy
thys/Uncomputable.thy
--- a/thys/Abacus.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Abacus.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/Abacus.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Abacus Machines *}
--- a/thys/Abacus_Defs.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Abacus_Defs.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/Abacus.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Alternative Definitions for Translating Abacus Machines to TMs *}
--- a/thys/Abacus_Hoare.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Abacus_Hoare.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,3 +1,8 @@
+(* Title: thys/Abacus_Hoare.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
+*)
+
 theory Abacus_Hoare
 imports Abacus
 begin
--- a/thys/Abacus_Mopup.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Abacus_Mopup.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/Abacus_Mopup.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Mopup Turing Machine that deletes all "registers", except one *}
--- a/thys/Rec_Def.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Rec_Def.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,3 +1,8 @@
+(* Title: thys/Rec_Def.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
+*)
+
 theory Rec_Def
 imports Main
 begin
--- a/thys/Recursive.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Recursive.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,3 +1,8 @@
+(* Title: thys/Recursive.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
+*)
+
 theory Recursive
 imports Abacus Rec_Def Abacus_Hoare
 begin
--- a/thys/Turing.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Turing.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/Turing.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Turing Machines *}
--- a/thys/Turing_Hoare.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Turing_Hoare.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/Turing_Hoare.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Hoare Rules for TMs *}
--- a/thys/UF.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/UF.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/UF.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Construction of a Universal Function *}
--- a/thys/UTM.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/UTM.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/UTM.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Construction of a Universal Turing Machine *}
--- a/thys/Uncomputable.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Uncomputable.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,5 +1,6 @@
 (* Title: thys/Uncomputable.thy
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
 *)
 
 chapter {* Undeciablity of the Halting Problem *}