--- a/QuotMain.thy Sat Oct 17 16:06:54 2009 +0200
+++ b/QuotMain.thy Sun Oct 18 00:52:10 2009 +0200
@@ -3,6 +3,7 @@
uses ("quotient.ML")
begin
+
locale QUOT_TYPE =
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -141,6 +142,7 @@
end
+
section {* type definition for the quotient type *}
use "quotient.ML"
@@ -250,7 +252,6 @@
ML {* lookup @{theory} @{type_name list} *}
-
ML {*
(* calculates the aggregate abs and rep functions for a given type;
repF is for constants' arguments; absF is for constants;