Quot/Examples/AbsRepTest.thy
changeset 1097 551eacf071d7
parent 922 a2589b4bc442
child 1128 17ca92ab4660
--- a/Quot/Examples/AbsRepTest.thy	Tue Feb 09 14:32:37 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Tue Feb 09 15:28:15 2010 +0100
@@ -105,62 +105,62 @@
   by (auto simp add: equivp_def expand_fun_eq)
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "nat \<times> nat"}, 
       @{typ "myint"})
 *}
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "('a * 'a) list"}, 
       @{typ "'a foo"})
 *}
 
 ML {*
-test_funs repF @{context} 
+test_funs RepF @{context} 
      (@{typ "(('a * 'a) list * 'b)"}, 
       @{typ "('a foo * 'b)"})
 *}
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "(('a list) * int) list"}, 
       @{typ "('a fset) bar"})
 *}
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "('a list)"}, 
       @{typ "('a fset)"})
 *}
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "('a list) list"}, 
       @{typ "('a fset) fset"})
 *}
 
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "((nat * nat) list) list"}, 
       @{typ "((myint) fset) fset"})
 *}
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "(('a * 'a) list) list"}, 
       @{typ "(('a * 'a) fset) fset"})
 *}
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
       (@{typ "(nat * nat) list"}, 
        @{typ "myint fset"})
 *}
 
 ML {*
-test_funs absF @{context} 
+test_funs AbsF @{context} 
      (@{typ "('a list) list \<Rightarrow> 'a list"}, 
       @{typ "('a fset) fset \<Rightarrow> 'a fset"})
 *}