Quot/quotient_def.ML
changeset 789 8237786171f1
parent 776 d1064fa29424
child 799 0755f8fd56b3
--- a/Quot/quotient_def.ML	Fri Dec 25 00:17:55 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 25 00:58:06 2009 +0100
@@ -3,6 +3,7 @@
 sig 
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     local_theory -> (term * thm) * local_theory
+
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
 end;