--- a/src/HOL/Library/SCT_Interpretation.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Interpretation.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,8 +1,12 @@
+(* Title: HOL/Library/SCT_Interpretation.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Interpretation
imports Main SCT_Misc SCT_Definition
begin
-
definition
"idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))"
@@ -409,5 +413,4 @@
thus "acc R x" ..
qed
-
-end
\ No newline at end of file
+end