--- a/thys/Paper/Paper.thy	Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/Paper/Paper.thy	Thu Feb 25 12:17:31 2016 +0000
@@ -16,8 +16,8 @@
   Sequ ("_ @ _" [78,77] 63) and
   injval ("inj _ _ _" [1000,77,1000] 77) and 
   projval ("proj _ _ _" [1000,77,1000] 77) and 
-  length ("len _" [78] 73) and
-  ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73)
+  length ("len _" [78] 73) 
+  (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *)
 (*>*)
 
 section {* Introduction *}
@@ -328,24 +328,6 @@
   to the cases above.
 *}
 
-text {*
-  \noindent
-  Things we have proved about our version of the Sulzmann ordering
-
-  \begin{center}
-  \begin{tabular}{c}
-  @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\
-  %@ {thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]}
-  \end{tabular}
-  \end{center}\bigskip  
-
-  \noindent
-  Things we like to prove, but cannot:\bigskip
-
-  If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"}
-  
-*}
-
 
 text {*
   %\noindent