Quot/Examples/AbsRepTest.thy
changeset 807 a5495a323b49
parent 803 6f6ee78c7357
child 808 90bde96f5dd1
--- 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"})
 *}