--- a/Precedence_ord.thy	Tue May 06 14:36:40 2014 +0100
+++ b/Precedence_ord.thy	Thu May 15 16:02:44 2014 +0100
@@ -27,8 +27,19 @@
 
 instance precedence :: preorder ..
 
-instance precedence :: linorder proof
+instance precedence :: linorder 
+proof
 qed (auto simp: precedence_le_def precedence_less_def 
               intro: order_trans split:precedence.splits)
 
+instantiation precedence :: zero
+begin
+
+definition Zero_precedence_def:
+  "0 = Prc 0 0"
+
+instance ..
+
 end
+
+end