--- a/src/HOL/Library/SCT_Examples.thy Wed Feb 28 10:36:10 2007 +0100
+++ b/src/HOL/Library/SCT_Examples.thy Wed Feb 28 11:12:12 2007 +0100
@@ -1,9 +1,12 @@
+(* Title: HOL/Library/SCT_Examples.thy
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+*)
+
theory SCT_Examples
imports Size_Change_Termination
begin
-
-
function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"f n 0 = n"
@@ -23,7 +26,6 @@
apply (rule SCT'_exec)
by eval (* Evaluate to true *)
-
function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
"p m n r = (if r>0 then p m (r - 1) n else
@@ -61,7 +63,6 @@
apply (rule SCT'_exec)
by eval
-
function (sequential)
bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
@@ -79,5 +80,4 @@
apply (simp add:finite_acg_ins finite_acg_empty)
by (rule SCT'_empty)
-
-end
\ No newline at end of file
+end