--- a/thys/Hoare_gen.thy	Thu Mar 06 15:28:20 2014 +0000
+++ b/thys/Hoare_gen.thy	Thu Mar 13 20:06:29 2014 +0000
@@ -4,12 +4,9 @@
 
 theory Hoare_gen
 imports Main  
-  (*"../progtut/Tactical" *)
   "../Separation_Algebra/Sep_Tactics"
 begin
 
-ML_file "../Separation_Algebra/sep_tactics.ML"
-
 definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)
 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"