--- a/QuotScript.thy Wed Oct 14 16:23:49 2009 +0200 +++ b/QuotScript.thy Wed Oct 14 18:13:16 2009 +0200 @@ -416,3 +416,4 @@ using a by (metis EQUIV_def IN_RESPECTS a) end +