diff -r 43336511993f -r a5495a323b49 Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Tue Jan 05 10:41:20 2010 +0100 +++ b/Quot/Examples/AbsRepTest.thy Tue Jan 05 14:09:04 2010 +0100 @@ -11,7 +11,10 @@ |> writeln; equiv_relation_chk ctxt (rty, qty) |> Syntax.string_of_term ctxt - |> writeln) + |> writeln; + new_equiv_relation_chk ctxt (rty, qty) + |> Syntax.string_of_term ctxt + |> writeln) *} definition @@ -81,6 +84,12 @@ ML {* test_funs absF @{context} + (@{typ "('a list)"}, + @{typ "('a fset)"}) +*} + +ML {* +test_funs absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"}) *}