--- a/LamEx.thy Fri Dec 04 09:25:27 2009 +0100 +++ b/LamEx.thy Fri Dec 04 09:33:32 2009 +0100 @@ -340,5 +340,3 @@ (*apply (tactic {* regularize_tac @{context} 1 *})*) sorry -done -