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