diff -r 2c56b20032a7 -r 0679a84b11ad prio/Precedence_ord.thy
--- a/prio/Precedence_ord.thy	Mon Dec 03 08:16:58 2012 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +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)
-
-end