
diff -r 331873ebc5cd -r 7aa18bae6983 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Aug 25 09:02:06 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Wed Aug 25 11:58:37 2010 +0800
@@ -68,8 +68,6 @@
     prod.cases}
 *}
 
-(*  HERE *)
-
 ML {*
  val thms_e = map (lift_thm @{context} qtys simps)  @{thms eq_iff}
 *}
@@ -97,12 +95,6 @@
 
 
 
-ML {*
-  space_explode "_raw" "bla_raw2_foo_raw3.0"
-*}
-
-
-
 thm eq_iff
 
 thm lam.fv




