# HG changeset patch
# User wenzelm
# Date 1734019629 -3600
# Node ID adbd2e1407cc8362ca1ea1d519994343290dad0a
# Parent  a065d8bcfd3df9da9ea43915bf03f62ed2526bcf
tuned proofs;

diff -r a065d8bcfd3d -r adbd2e1407cc src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Thu Dec 12 16:57:06 2024 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Thu Dec 12 17:07:09 2024 +0100
@@ -24,9 +24,9 @@
   apply (rule class.po.intro)
   apply (unfold below)
     apply (rule below_refl)
-   apply (erule (1) below_trans)
+   apply (fact below_trans)
   apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
-  apply (erule (1) below_antisym)
+  apply (fact below_antisym)
   done
 
 lemmas typedef_po_class = below.typedef_class_po [THEN po.intro_of_class]