--- a/Precedence_ord.thy~	Thu Jan 28 21:14:17 2016 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-header {* Order on product types *}
-
-theory Precedence_ord
-imports Main
-begin
-
-datatype precedence = Prc nat nat
-
-instantiation precedence :: order
-begin
-
-definition
-  precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of
-                                   (Prc fx sx, Prc fy sy) \<Rightarrow> 
-                                 fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))"
-
-definition
-  precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of
-                               (Prc fx sx, Prc fy sy) \<Rightarrow> 
-                                     fx < fy \<or> (fx \<le> fy \<and> sy < sx))"
-
-instance
-proof
-qed (auto simp: precedence_le_def precedence_less_def 
-              intro: order_trans split:precedence.splits)
-end
-
-instance precedence :: preorder ..
-
-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