# HG changeset patch
# User wenzelm
# Date 1636037841 -3600
# Node ID 55a4b319b2b9a7ec99facb8186bce357f6d748dc
# Parent  23a97a547a9ef6f7a61b45febe1c4b1314625596
tuned whitespace;

diff -r 23a97a547a9e -r 55a4b319b2b9 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Thu Nov 04 15:54:01 2021 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Nov 04 15:57:21 2021 +0100
@@ -45,10 +45,8 @@
   have F1: "\<forall>x\<^sub>1::'a::linordered_idom. 0 \<le> \<bar>x\<^sub>1\<bar>" by (metis abs_ge_zero)
   have F2: "\<forall>x\<^sub>1::'a::linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1)
   have F3: "\<forall>x\<^sub>1 x\<^sub>3. x\<^sub>3 \<le> \<bar>h x\<^sub>1\<bar> \<longrightarrow> x\<^sub>3 \<le> c * \<bar>f x\<^sub>1\<bar>" by (metis A1 order_trans)
-  have F4: "\<forall>x\<^sub>2 x\<^sub>3::'a::linordered_idom. \<bar>x\<^sub>3\<bar> * \<bar>x\<^sub>2\<bar> = \<bar>x\<^sub>3 * x\<^sub>2\<bar>"
-    by (metis abs_mult)
-  have F5: "\<forall>x\<^sub>3 x\<^sub>1::'a::linordered_idom. 0 \<le> x\<^sub>1 \<longrightarrow> \<bar>x\<^sub>3 * x\<^sub>1\<bar> = \<bar>x\<^sub>3\<bar> * x\<^sub>1"
-    by (metis abs_mult_pos)
+  have F4: "\<forall>x\<^sub>2 x\<^sub>3::'a::linordered_idom. \<bar>x\<^sub>3\<bar> * \<bar>x\<^sub>2\<bar> = \<bar>x\<^sub>3 * x\<^sub>2\<bar>" by (metis abs_mult)
+  have F5: "\<forall>x\<^sub>3 x\<^sub>1::'a::linordered_idom. 0 \<le> x\<^sub>1 \<longrightarrow> \<bar>x\<^sub>3 * x\<^sub>1\<bar> = \<bar>x\<^sub>3\<bar> * x\<^sub>1" by (metis abs_mult_pos)
   hence "\<forall>x\<^sub>1\<ge>0. \<bar>x\<^sub>1::'a::linordered_idom\<bar> = \<bar>1\<bar> * x\<^sub>1" by (metis F2)
   hence "\<forall>x\<^sub>1\<ge>0. \<bar>x\<^sub>1::'a::linordered_idom\<bar> = x\<^sub>1" by (metis F2 abs_one)
   hence "\<forall>x\<^sub>3. 0 \<le> \<bar>h x\<^sub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^sub>3\<bar>\<bar> = c * \<bar>f x\<^sub>3\<bar>" by (metis F3)