--- a/Quot/Examples/IntEx.thy Mon Jan 11 01:03:34 2010 +0100 +++ b/Quot/Examples/IntEx.thy Mon Jan 11 11:51:19 2010 +0100 @@ -199,6 +199,8 @@ apply simp done + +term foldl lemma "foldl PLUS x [] = x" apply(lifting ho_tst) done