QuotTest.thy
changeset 180 fcacca9588b4
parent 177 bdfe4388955d
child 185 929bc55efff7
--- a/QuotTest.thy	Sat Oct 24 17:29:20 2009 +0200
+++ b/QuotTest.thy	Sat Oct 24 18:17:38 2009 +0200
@@ -72,7 +72,6 @@
 quotient qt = "t" / "Rt"
   by (rule t_eq)
 
-
 ML {*
   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst