Nominal/Ex/Lambda.thy
changeset 2432 7aa18bae6983
parent 2431 331873ebc5cd
child 2434 92dc6cfa3a95
--- 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