--- a/src/HOL/Library/Size_Change_Termination.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/Size_Change_Termination.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,12 +1,13 @@
+(* Title: HOL/Library/Size_Change_Termination.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory Size_Change_Termination
imports SCT_Theorem SCT_Interpretation SCT_Implementation
uses "size_change_termination.ML"
begin
-use "size_change_termination.ML"
-
-
-
section {* Simplifier setup *}
text {* This is needed to run the SCT algorithm in the simplifier: *}
@@ -99,6 +100,4 @@
lemmas sctTest_congs =
if_weak_cong let_weak_cong setbcomp_cong
-
-
-end
\ No newline at end of file
+end