--- a/thys/Abacus.thy	Mon Feb 18 13:26:27 2013 +0000
+++ b/thys/Abacus.thy	Mon Feb 18 13:28:51 2013 +0000
@@ -19,31 +19,6 @@
   
 type_synonym abc_prog = "abc_inst list"
 
-section {* Some Sample Abacus programs *}
-
-(* Abacus for addition and clearance *)
-fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"  
-  where
-  "plus_clear m n e = [Dec m e, Inc n, Goto 0]"
-
-(* Abacus for clearing memory untis *)
-fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
-  where
-  "clear n e = [Dec n e, Goto 0]"
-
-fun plus:: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
-  where
-  "plus m n p e = [Dec m 4, Inc n, Inc p,
-                   Goto 0, Dec p e, Inc m, Goto 4]"
-
-fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
-  where
-  "mult m1 m2 n p e = [Dec m1 e]@ plus m2 n p 1"
-
-fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
-  where
-  "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2"
-
 type_synonym abc_state = nat
 
 text {*