src/HOL/Library/Size_Change_Termination.thy

--- a/src/HOL/Library/Size_Change_Termination.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/Size_Change_Termination.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header "Size-Change Termination"
 
 theory Size_Change_Termination
 imports SCT_Theorem SCT_Interpretation SCT_Implementation 
@@ -102,4 +102,10 @@
 lemmas sctTest_congs = 
   if_weak_cong let_weak_cong setbcomp_cong
 
+
+lemma SCT_Main:
+  "finite_acg A \<Longrightarrow> test_SCT A \<Longrightarrow> SCT A"
+  using LJA_Theorem4 SCT'_exec
+  by auto
+
 end