diff -r e576a97e9a3e -r 1bf4337919d3 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Thu Jan 21 09:02:04 2010 +0100 +++ b/Quot/Examples/IntEx.thy Thu Jan 21 09:55:05 2010 +0100 @@ -186,6 +186,15 @@ using a b c by (lifting int_induct_raw) +lemma ex1tst: "\! (x :: nat \ nat) \ Respects (op \). True" +sorry + +lemma ex1tst': "\! (x :: my_int). True" +apply(lifting ex1tst) +apply(cleaning) +apply simp +sorry + lemma ho_tst: "foldl my_plus x [] = x" apply simp done