Loading theory "HOL-Library.Adhoc_Overloading" (required by "IEEE_Floating_Point.Double" via "HOL-Library.Monad_Syntax") Loading theory "HOL-Library.Code_Abstract_Nat" (required by "IEEE_Floating_Point.Double" via "IEEE_Floating_Point.Conversion_IEEE_Float" via "HOL-Library.Code_Target_Numeral" via "HOL-Library.Code_Target_Nat") ### theory "HOL-Library.Code_Abstract_Nat" ### 0.109s elapsed time, 0.300s cpu time, 0.000s GC time Loading theory "HOL-Library.Code_Target_Nat" (required by "IEEE_Floating_Point.Double" via "IEEE_Floating_Point.Conversion_IEEE_Float" via "HOL-Library.Code_Target_Numeral") signature ADHOC_OVERLOADING = sig val generic_add_overloaded: string -> Context.generic -> Context.generic val generic_add_variant: string -> term -> Context.generic -> Context.generic val generic_remove_overloaded: string -> Context.generic -> Context.generic val generic_remove_variant: string -> term -> Context.generic -> Context.generic val is_overloaded: Proof.context -> string -> bool val show_variants: bool Config.T end structure Adhoc_Overloading: ADHOC_OVERLOADING ### theory "HOL-Library.Adhoc_Overloading" ### 0.163s elapsed time, 0.408s cpu time, 0.000s GC time Loading theory "HOL-Library.Monad_Syntax" (required by "IEEE_Floating_Point.Double") ### Code generator: dropping subsumed code equation ### divmod_nat ?m ?n \ ### if ?n = 0 \ ?m < ?n then (0, ?m) ### else let (q, y) = divmod_nat (?m - ?n) ?n in (Suc q, y) ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) (num.Bit1 ?n) \ ### if ?m < ?n then (0, numeral (num.Bit1 ?m)) ### else divmod_step (num.Bit1 ?n) ### (divmod (num.Bit1 ?m) (num.Bit0 (num.Bit1 ?n))) ### theory "HOL-Library.Monad_Syntax" ### 0.051s elapsed time, 0.104s cpu time, 0.000s GC time Loading theory "HOL-Library.Code_Target_Int" (required by "IEEE_Floating_Point.Double" via "IEEE_Floating_Point.Conversion_IEEE_Float" via "HOL-Library.Code_Target_Numeral") ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) (num.Bit1 ?n) \ ### if ?m \ ?n then (0, numeral (num.Bit0 ?m)) ### else divmod_step (num.Bit1 ?n) ### (divmod (num.Bit0 ?m) (num.Bit0 (num.Bit1 ?n))) ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) (num.Bit0 ?n) \ ### case divmod ?m ?n of (q, r) \ (q, 2 * r + 1) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) (num.Bit0 ?n) \ ### case divmod ?m ?n of (q, r) \ (q, 2 * r) ### Code generator: dropping subsumed code equation ### divmod num.One (num.Bit1 ?n) \ (0, Numeral1) ### Code generator: dropping subsumed code equation ### divmod num.One (num.Bit0 ?n) \ (0, Numeral1) ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) num.One \ (numeral (num.Bit1 ?m), 0) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) num.One \ (numeral (num.Bit0 ?m), 0) ### Code generator: dropping subsumed code equation ### divmod num.One num.One \ (Numeral1, 0) ### Code generator: dropping subsumed code equation ### Suc ?m \ ?n \ ?m < ?n ### Code generator: dropping subsumed code equation ### 0 \ ?n \ True ### Code generator: dropping subsumed code equation ### ?m < Suc ?n \ ?m \ ?n ### Code generator: dropping subsumed code equation ### ?n < 0 \ False ### Code generator: dropping subsumed code equation ### of_nat ?n \ ### semiring_1_class.of_nat_aux (\i. i + (1::?'a)) ?n (0::?'a) ### Code generator: dropping subsumed code equation ### 1 \ Int.Pos num.One ### Code generator: dropping subsumed code equation ### Int.Neg ?m + Int.Neg ?n \ Int.Neg (?m + ?n) ### Code generator: dropping subsumed code equation ### Int.Neg ?m + Int.Pos ?n \ Int.sub ?n ?m ### Code generator: dropping subsumed code equation ### Int.Pos ?m + Int.Neg ?n \ Int.sub ?m ?n ### Code generator: dropping subsumed code equation ### Int.Pos ?m + Int.Pos ?n \ Int.Pos (?m + ?n) ### Code generator: dropping subsumed code equation ### 0 + ?l \ ?l ### Code generator: dropping subsumed code equation ### ?k + 0 \ ?k ### Code generator: dropping subsumed code equation ### - Int.Neg ?m \ Int.Pos ?m ### Code generator: dropping subsumed code equation ### - Int.Pos ?m \ Int.Neg ?m ### Code generator: dropping subsumed code equation ### - 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m - Int.Neg ?n \ Int.sub ?n ?m ### Code generator: dropping subsumed code equation ### Int.Neg ?m - Int.Pos ?n \ Int.Neg (?m + ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m - Int.Neg ?n \ Int.Pos (?m + ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m - Int.Pos ?n \ Int.sub ?m ?n ### Code generator: dropping subsumed code equation ### 0 - ?l \ - ?l ### Code generator: dropping subsumed code equation ### ?k - 0 \ ?k ### Code generator: dropping subsumed code equation ### Int.dup (Int.Neg ?n) \ Int.Neg (num.Bit0 ?n) ### Code generator: dropping subsumed code equation ### Int.dup (Int.Pos ?n) \ Int.Pos (num.Bit0 ?n) ### Code generator: dropping subsumed code equation ### Int.dup 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m * Int.Neg ?n \ Int.Pos (?m * ?n) ### Code generator: dropping subsumed code equation ### Int.Neg ?m * Int.Pos ?n \ Int.Neg (?m * ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m * Int.Neg ?n \ Int.Neg (?m * ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m * Int.Pos ?n \ Int.Pos (?m * ?n) ### Code generator: dropping subsumed code equation ### 0 * ?l \ 0 ### Code generator: dropping subsumed code equation ### ?k * 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m div Int.Neg ?n \ fst (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m div Int.Neg ?n \ - Divides.adjust_div (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Neg ?m div Int.Pos ?n \ - Divides.adjust_div (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m div Int.Pos ?n \ fst (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### ?k div Int.Neg num.One \ - ?k ### Code generator: dropping subsumed code equation ### ?k div Int.Pos num.One \ ?k ### Code generator: dropping subsumed code equation ### 0 div ?k \ 0 ### Code generator: dropping subsumed code equation ### ?k div 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m mod Int.Neg ?n \ - snd (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m mod Int.Neg ?n \ ### - Divides.adjust_mod (Int.Pos ?n) (snd (divmod ?m ?n)) ### Code generator: dropping subsumed code equation ### Int.Neg ?m mod Int.Pos ?n \ ### Divides.adjust_mod (Int.Pos ?n) (snd (divmod ?m ?n)) ### Code generator: dropping subsumed code equation ### Int.Pos ?m mod Int.Pos ?n \ snd (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### ?k mod Int.Neg num.One \ 0 ### Code generator: dropping subsumed code equation ### ?k mod Int.Pos num.One \ 0 ### Code generator: dropping subsumed code equation ### 0 mod ?k \ 0 ### Code generator: dropping subsumed code equation ### ?k mod 0 \ ?k ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) (num.Bit1 ?n) \ ### if ?m < ?n then (0, numeral (num.Bit1 ?m)) ### else divmod_step (num.Bit1 ?n) ### (divmod (num.Bit1 ?m) (num.Bit0 (num.Bit1 ?n))) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) (num.Bit1 ?n) \ ### if ?m \ ?n then (0, numeral (num.Bit0 ?m)) ### else divmod_step (num.Bit1 ?n) ### (divmod (num.Bit0 ?m) (num.Bit0 (num.Bit1 ?n))) ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) (num.Bit0 ?n) \ ### case divmod ?m ?n of (q, r) \ (q, 2 * r + 1) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) (num.Bit0 ?n) \ ### case divmod ?m ?n of (q, r) \ (q, 2 * r) ### Code generator: dropping subsumed code equation ### divmod num.One (num.Bit1 ?n) \ (0, Numeral1) ### Code generator: dropping subsumed code equation ### divmod num.One (num.Bit0 ?n) \ (0, Numeral1) ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) num.One \ (numeral (num.Bit1 ?m), 0) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) num.One \ (numeral (num.Bit0 ?m), 0) ### Code generator: dropping subsumed code equation ### divmod num.One num.One \ (Numeral1, 0) ### Code generator: dropping subsumed code equation ### equal_class.equal ?k ?k \ True ### theory "HOL-Library.Code_Target_Nat" ### 0.201s elapsed time, 0.408s cpu time, 0.000s GC time ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Neg ?k) (Int.Neg ?l) \ equal_class.equal ?k ?l Loading theory "HOL-Library.Lattice_Algebras" (required by "IEEE_Floating_Point.IEEE_Properties" via "IEEE_Floating_Point.IEEE" via "HOL-Library.Float") ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Neg ?k) (Int.Pos ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Neg ?k) 0 \ False ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Pos ?k) (Int.Neg ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Pos ?k) (Int.Pos ?l) \ equal_class.equal ?k ?l ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Pos ?k) 0 \ False ### Code generator: dropping subsumed code equation ### equal_class.equal 0 (Int.Neg ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal 0 (Int.Pos ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal 0 0 \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k \ Int.Neg ?l \ ?l \ ?k ### Code generator: dropping subsumed code equation ### Int.Neg ?k \ Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k \ 0 \ True ### Code generator: dropping subsumed code equation ### Int.Pos ?k \ Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### Int.Pos ?k \ Int.Pos ?l \ ?k \ ?l ### Code generator: dropping subsumed code equation ### Int.Pos ?k \ 0 \ False ### Code generator: dropping subsumed code equation ### 0 \ Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### 0 \ Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### 0 \ 0 \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k < Int.Neg ?l \ ?l < ?k ### Code generator: dropping subsumed code equation ### Int.Neg ?k < Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k < 0 \ True ### Code generator: dropping subsumed code equation ### Int.Pos ?k < Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### Int.Pos ?k < Int.Pos ?l \ ?k < ?l ### Code generator: dropping subsumed code equation ### Int.Pos ?k < 0 \ False ### Code generator: dropping subsumed code equation ### 0 < Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### 0 < Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### 0 < 0 \ False ### Code generator: dropping subsumed code equation ### of_int (Int.Pos ?k) \ numeral ?k ### Code generator: dropping subsumed code equation ### of_int 0 \ 0::?'a ### Code generator: dropping subsumed code equation ### of_int (Int.Neg ?k) \ - numeral ?k ### Code generator: dropping subsumed code equation ### nat (Int.Pos ?k) \ nat_of_num ?k ### Code generator: dropping subsumed code equation ### nat 0 \ 0 ### Code generator: dropping subsumed code equation ### nat (Int.Neg ?k) \ 0 ### theory "HOL-Library.Code_Target_Int" ### 0.205s elapsed time, 0.412s cpu time, 0.000s GC time Loading theory "HOL-Library.Code_Target_Numeral" (required by "IEEE_Floating_Point.Double" via "IEEE_Floating_Point.Conversion_IEEE_Float") ### theory "HOL-Library.Code_Target_Numeral" ### 0.159s elapsed time, 0.320s cpu time, 0.000s GC time Loading theory "HOL-Library.Log_Nat" (required by "IEEE_Floating_Point.IEEE_Properties" via "IEEE_Floating_Point.IEEE" via "HOL-Library.Float") ### theory "HOL-Library.Log_Nat" ### 0.208s elapsed time, 0.416s cpu time, 0.000s GC time ### Ignoring duplicate rewrite rule: ### of_nat (?m1 * ?n1) \ of_nat ?m1 * of_nat ?n1 ### Ignoring duplicate rewrite rule: ### of_nat (?m1 * ?n1) \ of_nat ?m1 * of_nat ?n1 ### Ignoring duplicate rewrite rule: ### sup ?x1 (sup ?x1 ?y1) \ sup ?x1 ?y1 class lattice_ab_group_add_abs = abs + lattice_ab_group_add + assumes "abs_lattice": "\a. \a\ = sup a (- a)" ### theory "HOL-Library.Lattice_Algebras" ### 4.645s elapsed time, 8.040s cpu time, 0.224s GC time Loading theory "HOL-Library.Float" (required by "IEEE_Floating_Point.IEEE_Properties" via "IEEE_Floating_Point.IEEE") instantiation float :: {equal,linordered_idom} sgn_float == sgn :: float \ float abs_float == abs :: float \ float uminus_float == uminus :: float \ float one_float == one_class.one :: float times_float == times :: float \ float \ float zero_float == zero_class.zero :: float minus_float == minus :: float \ float \ float less_eq_float == less_eq :: float \ float \ bool less_float == less :: float \ float \ bool plus_float == plus :: float \ float \ float equal_float == equal_class.equal :: float \ float \ bool instantiation float :: lattice_ab_group_add inf_float == inf :: float \ float \ float sup_float == sup :: float \ float \ float instantiation float :: exhaustive exhaustive_float == exhaustive_class.exhaustive :: (float \ (bool \ term list) option) \ natural \ (bool \ term list) option instantiation float :: full_exhaustive full_exhaustive_float == full_exhaustive_class.full_exhaustive :: (float \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option instantiation float :: random random_float == random_class.random :: natural \ natural \ natural \ (float \ (unit \ term)) \ natural \ natural Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### mantissa 0 \ 0 ### theory "HOL-Library.Float" ### 2.558s elapsed time, 5.092s cpu time, 0.276s GC time Loading theory "IEEE_Floating_Point.IEEE" (required by "IEEE_Floating_Point.IEEE_Properties") ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Word.word" found. instantiation IEEE.float :: (len, len) zero zero_float == zero_class.zero :: ('a, 'b) IEEE.float instantiation IEEE.float :: (len, len) uminus uminus_float == uminus :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float Found termination order: "{}" Found termination order: "{}" instantiation IEEE.float :: (len, len) plus plus_float == plus :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float instantiation IEEE.float :: (len, len) minus minus_float == minus :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float instantiation IEEE.float :: (len, len) times times_float == times :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float instantiation IEEE.float :: (len, len) one one_float == one_class.one :: ('a, 'b) IEEE.float instantiation IEEE.float :: (len, len) inverse inverse_float == inverse :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float divide_float == divide :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float instantiation IEEE.float :: (len, len) ord less_eq_float == less_eq :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float \ bool less_float == less :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float \ bool instantiation IEEE.float :: (len, len) abs abs_float == abs :: ('a, 'b) IEEE.float \ ('a, 'b) IEEE.float ### theory "IEEE_Floating_Point.IEEE" ### 3.720s elapsed time, 7.372s cpu time, 0.756s GC time Loading theory "IEEE_Floating_Point.IEEE_Properties" Loading theory "IEEE_Floating_Point.FP64" ### theory "IEEE_Floating_Point.IEEE_Properties" ### 0.654s elapsed time, 1.312s cpu time, 0.000s GC time Loading theory "IEEE_Floating_Point.Conversion_IEEE_Float" (required by "IEEE_Floating_Point.Double") ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Numeral_Type.bit0" found. ### theory "IEEE_Floating_Point.FP64" ### 0.924s elapsed time, 1.856s cpu time, 0.000s GC time ### theory "IEEE_Floating_Point.Conversion_IEEE_Float" ### 0.557s elapsed time, 1.116s cpu time, 0.000s GC time Loading theory "IEEE_Floating_Point.Double" ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Numeral_Type.bit0" found. instantiation double :: {inverse,abs,minus,one,plus,times,uminus,zero,ord} less_eq_double == less_eq :: double \ double \ bool less_double == less :: double \ double \ bool zero_double == zero_class.zero :: double uminus_double == uminus :: double \ double times_double == times :: double \ double \ double plus_double == plus :: double \ double \ double one_double == one_class.one :: double minus_double == minus :: double \ double \ double abs_double == abs :: double \ double inverse_double == inverse :: double \ double divide_double == divide :: double \ double \ double Found termination order: "size <*mlex*> {}" structure Orderings : sig type 'a ord val less_eq : 'a ord -> 'a -> 'a -> bool val less : 'a ord -> 'a -> 'a -> bool val max : 'a ord -> 'a -> 'a -> 'a end = struct type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool}; val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool; val less = #less : 'a ord -> 'a -> 'a -> bool; fun max A_ a b = (if less_eq A_ a b then b else a); end; (*struct Orderings*) structure Arith : sig type nat type num val one_nat : nat val zero_nat : nat val equal_nat : nat -> nat -> bool val minus_nat : nat -> nat -> nat end = struct val ord_integer = {less_eq = (fn a => fn b => IntInf.<= (a, b)), less = (fn a => fn b => IntInf.< (a, b))} : IntInf.int Orderings.ord; datatype nat = Nat of IntInf.int; datatype num = One | Bit0 of num | Bit1 of num; val one_nat : nat = Nat (1 : IntInf.int); val zero_nat : nat = Nat (0 : IntInf.int); fun integer_of_nat (Nat x) = x; fun equal_nat m n = (((integer_of_nat m) : IntInf.int) = (integer_of_nat n)); fun minus_nat m n = Nat (Orderings.max ord_integer (0 : IntInf.int) (IntInf.- (integer_of_nat m, integer_of_nat n))); end; (*struct Arith*) structure Double : sig val float_of : Arith.nat -> real end = struct fun float_of n = (if Arith.equal_nat n Arith.zero_nat then 0.0 else Real.+ (float_of (Arith.minus_nat n Arith.one_nat), 1.0)); end; (*struct Double*) consts check_all :: "nat \ (nat \ bool) \ bool" ### theory "IEEE_Floating_Point.Double" ### 1.889s elapsed time, 3.744s cpu time, 0.332s GC time ### Metis: Unused theorems: "Float.zero_float.abs_eq" ### Metis: Unused theorems: "Archimedean_Field.floor_less_cancel" *** Failed to finish proof (line 122 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy"): *** goal (2 subgoals): *** 1. 0 < unat max_word *** 2. 0 < unat max_word *** At command "by" (line 122 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy") *** Undefined fact: "p2_eq_1" (line 1030 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy") *** At command "by" (line 1030 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy") *** Undefined fact: "word_cat_inj" (line 33 of "~~/afp/thys/IEEE_Floating_Point/FP64.thy") *** At command "by" (line 33 of "~~/afp/thys/IEEE_Floating_Point/FP64.thy") linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) ### Ignoring duplicate rewrite rule: ### ?n1 \ ?m1 \ ### of_nat (?m1 - ?n1) \ of_nat ?m1 - of_nat ?n1 isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/IEEE_Floating_Point/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/IEEE_Floating_Point/document -o pdf -n document *** Undefined fact: "word_cat_inj" (line 33 of "~~/afp/thys/IEEE_Floating_Point/FP64.thy") *** At command "by" (line 33 of "~~/afp/thys/IEEE_Floating_Point/FP64.thy") *** Undefined fact: "p2_eq_1" (line 1030 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy") *** At command "by" (line 1030 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy") *** Failed to finish proof (line 122 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy"): *** goal (2 subgoals): *** 1. 0 < unat max_word *** 2. 0 < unat max_word *** At command "by" (line 122 of "~~/afp/thys/IEEE_Floating_Point/IEEE_Properties.thy")