--- a/thys2/PDerivs.thy	Wed Jan 12 15:24:10 2022 +0000
+++ b/thys2/PDerivs.thy	Wed Jan 12 17:08:46 2022 +0000
@@ -618,6 +618,8 @@
 text\<open>Antimirov's Theorem 3.8:\<close>
 lemma Maxsubterms38:
   shows "\<forall>pt \<in> (pders_Set UNIV t). pt \<in> (subs t) \<or> pt = ONE \<or> pt = (SEQ t0 t1)"
+  oops
+