diff options
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_num.thy')
| -rw-r--r-- | snapshots/isabelle/lib/lem/Lem_num.thy | 181 |
1 files changed, 90 insertions, 91 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_num.thy b/snapshots/isabelle/lib/lem/Lem_num.thy index ddbdd533..8efe867b 100644 --- a/snapshots/isabelle/lib/lem/Lem_num.thy +++ b/snapshots/isabelle/lib/lem/Lem_num.thy @@ -1,21 +1,20 @@ -chapter \<open>Generated by Lem from num.lem.\<close> +chapter \<open>Generated by Lem from \<open>num.lem\<close>.\<close> theory "Lem_num" -imports - Main - "Lem_bool" - "Lem_basic_classes" - "~~/src/HOL/Word/Word" - "Real" - "~~/src/HOL/NthRoot" +imports + Main + "Lem_bool" + "Lem_basic_classes" + "HOL-Word.Word" + "Complex_Main" begin (*open import Bool Basic_classes*) -(*open import {isabelle} `~~/src/HOL/Word/Word` `Real` `~~/src/HOL/NthRoot`*) +(*open import {isabelle} `HOL-Word.Word` `Complex_Main`*) (*open import {hol} `integerTheory` `intReduce` `wordsTheory` `wordsLib` `ratTheory` `realTheory` `intrealTheory` `transcTheory`*) (*open import {coq} `Coq.Numbers.BinNums` `Coq.ZArith.BinInt` `Coq.ZArith.Zpower` `Coq.ZArith.Zdiv` `Coq.ZArith.Zmax` `Coq.Numbers.Natural.Peano.NPeano` `Coq.QArith.Qabs` `Coq.QArith.Qminmax` `Coq.QArith.Qround` `Coq.Reals.ROrderedType` `Coq.Reals.Rbase` `Coq.Reals.Rfunctions`*) @@ -188,15 +187,15 @@ record 'a NumPred_class= definition instance_Basic_classes_Ord_nat_dict :: "(nat)Ord_class " where " instance_Basic_classes_Ord_nat_dict = ((| - compare_method = (genericCompare (op<) (op=)), + compare_method = (genericCompare (<) (=)), - isLess_method = (op<), + isLess_method = (<), - isLessEqual_method = (op \<le>), + isLessEqual_method = (\<le>), - isGreater_method = (op>), + isGreater_method = (>), - isGreaterEqual_method = (op \<ge>)|) )" + isGreaterEqual_method = (\<ge>)|) )" (*val natAdd : nat -> nat -> nat*) @@ -204,7 +203,7 @@ definition instance_Basic_classes_Ord_nat_dict :: "(nat)Ord_class " where definition instance_Num_NumAdd_nat_dict :: "(nat)NumAdd_class " where " instance_Num_NumAdd_nat_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val natMinus : nat -> nat -> nat*) @@ -212,7 +211,7 @@ definition instance_Num_NumAdd_nat_dict :: "(nat)NumAdd_class " where definition instance_Num_NumMinus_nat_dict :: "(nat)NumMinus_class " where " instance_Num_NumMinus_nat_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val natSucc : nat -> nat*) @@ -235,7 +234,7 @@ definition instance_Num_NumPred_nat_dict :: "(nat)NumPred_class " where definition instance_Num_NumMult_nat_dict :: "(nat)NumMult_class " where " instance_Num_NumMult_nat_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" (*val natDiv : nat -> nat -> nat*) @@ -243,13 +242,13 @@ definition instance_Num_NumMult_nat_dict :: "(nat)NumMult_class " where definition instance_Num_NumIntegerDivision_nat_dict :: "(nat)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_nat_dict = ((| - div_method = (op div)|) )" + div_method = (div)|) )" definition instance_Num_NumDivision_nat_dict :: "(nat)NumDivision_class " where " instance_Num_NumDivision_nat_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val natMod : nat -> nat -> nat*) @@ -257,7 +256,7 @@ definition instance_Num_NumDivision_nat_dict :: "(nat)NumDivision_class " wher definition instance_Num_NumRemainder_nat_dict :: "(nat)NumRemainder_class " where " instance_Num_NumRemainder_nat_dict = ((| - mod_method = (op mod)|) )" + mod_method = (mod)|) )" @@ -284,7 +283,7 @@ definition gen_pow :: " 'a \<Rightarrow>('a \<Rightarrow> 'a \<Rightarrow> 'a)\ definition instance_Num_NumPow_nat_dict :: "(nat)NumPow_class " where " instance_Num_NumPow_nat_dict = ((| - numPow_method = (op^)|) )" + numPow_method = (^)|) )" (*val natMin : nat -> nat -> nat*) @@ -318,15 +317,15 @@ definition instance_Basic_classes_OrdMaxMin_nat_dict :: "(nat)OrdMaxMin_class " definition instance_Basic_classes_Ord_Num_natural_dict :: "(nat)Ord_class " where " instance_Basic_classes_Ord_Num_natural_dict = ((| - compare_method = (genericCompare (op<) (op=)), + compare_method = (genericCompare (<) (=)), - isLess_method = (op<), + isLess_method = (<), - isLessEqual_method = (op \<le>), + isLessEqual_method = (\<le>), - isGreater_method = (op>), + isGreater_method = (>), - isGreaterEqual_method = (op \<ge>)|) )" + isGreaterEqual_method = (\<ge>)|) )" (*val naturalAdd : natural -> natural -> natural*) @@ -334,7 +333,7 @@ definition instance_Basic_classes_Ord_Num_natural_dict :: "(nat)Ord_class " wh definition instance_Num_NumAdd_Num_natural_dict :: "(nat)NumAdd_class " where " instance_Num_NumAdd_Num_natural_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val naturalMinus : natural -> natural -> natural*) @@ -342,7 +341,7 @@ definition instance_Num_NumAdd_Num_natural_dict :: "(nat)NumAdd_class " where definition instance_Num_NumMinus_Num_natural_dict :: "(nat)NumMinus_class " where " instance_Num_NumMinus_Num_natural_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val naturalSucc : natural -> natural*) @@ -365,7 +364,7 @@ definition instance_Num_NumPred_Num_natural_dict :: "(nat)NumPred_class " wher definition instance_Num_NumMult_Num_natural_dict :: "(nat)NumMult_class " where " instance_Num_NumMult_Num_natural_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" @@ -374,7 +373,7 @@ definition instance_Num_NumMult_Num_natural_dict :: "(nat)NumMult_class " wher definition instance_Num_NumPow_Num_natural_dict :: "(nat)NumPow_class " where " instance_Num_NumPow_Num_natural_dict = ((| - numPow_method = (op^)|) )" + numPow_method = (^)|) )" (*val naturalDiv : natural -> natural -> natural*) @@ -382,13 +381,13 @@ definition instance_Num_NumPow_Num_natural_dict :: "(nat)NumPow_class " where definition instance_Num_NumIntegerDivision_Num_natural_dict :: "(nat)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_natural_dict = ((| - div_method = (op div)|) )" + div_method = (div)|) )" definition instance_Num_NumDivision_Num_natural_dict :: "(nat)NumDivision_class " where " instance_Num_NumDivision_Num_natural_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val naturalMod : natural -> natural -> natural*) @@ -396,7 +395,7 @@ definition instance_Num_NumDivision_Num_natural_dict :: "(nat)NumDivision_class definition instance_Num_NumRemainder_Num_natural_dict :: "(nat)NumRemainder_class " where " instance_Num_NumRemainder_Num_natural_dict = ((| - mod_method = (op mod)|) )" + mod_method = (mod)|) )" (*val naturalMin : natural -> natural -> natural*) @@ -430,15 +429,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_natural_dict :: "(nat)OrdMaxMin definition instance_Basic_classes_Ord_Num_int_dict :: "(int)Ord_class " where " instance_Basic_classes_Ord_Num_int_dict = ((| - compare_method = (genericCompare (op<) (op=)), + compare_method = (genericCompare (<) (=)), - isLess_method = (op<), + isLess_method = (<), - isLessEqual_method = (op \<le>), + isLessEqual_method = (\<le>), - isGreater_method = (op>), + isGreater_method = (>), - isGreaterEqual_method = (op \<ge>)|) )" + isGreaterEqual_method = (\<ge>)|) )" (*val intNegate : int -> int*) @@ -462,7 +461,7 @@ definition instance_Num_NumAbs_Num_int_dict :: "(int)NumAbs_class " where definition instance_Num_NumAdd_Num_int_dict :: "(int)NumAdd_class " where " instance_Num_NumAdd_Num_int_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val intMinus : int -> int -> int*) @@ -470,7 +469,7 @@ definition instance_Num_NumAdd_Num_int_dict :: "(int)NumAdd_class " where definition instance_Num_NumMinus_Num_int_dict :: "(int)NumMinus_class " where " instance_Num_NumMinus_Num_int_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val intSucc : int -> int*) @@ -492,7 +491,7 @@ definition instance_Num_NumPred_Num_int_dict :: "(int)NumPred_class " where definition instance_Num_NumMult_Num_int_dict :: "(int)NumMult_class " where " instance_Num_NumMult_Num_int_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" @@ -501,7 +500,7 @@ definition instance_Num_NumMult_Num_int_dict :: "(int)NumMult_class " where definition instance_Num_NumPow_Num_int_dict :: "(int)NumPow_class " where " instance_Num_NumPow_Num_int_dict = ((| - numPow_method = (op^)|) )" + numPow_method = (^)|) )" (*val intDiv : int -> int -> int*) @@ -509,13 +508,13 @@ definition instance_Num_NumPow_Num_int_dict :: "(int)NumPow_class " where definition instance_Num_NumIntegerDivision_Num_int_dict :: "(int)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_int_dict = ((| - div_method = (op div)|) )" + div_method = (div)|) )" definition instance_Num_NumDivision_Num_int_dict :: "(int)NumDivision_class " where " instance_Num_NumDivision_Num_int_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val intMod : int -> int -> int*) @@ -523,7 +522,7 @@ definition instance_Num_NumDivision_Num_int_dict :: "(int)NumDivision_class " definition instance_Num_NumRemainder_Num_int_dict :: "(int)NumRemainder_class " where " instance_Num_NumRemainder_Num_int_dict = ((| - mod_method = (op mod)|) )" + mod_method = (mod)|) )" (*val intMin : int -> int -> int*) @@ -555,7 +554,7 @@ definition instance_Basic_classes_OrdMaxMin_Num_int_dict :: "(int)OrdMaxMin_cla definition instance_Basic_classes_Ord_Num_int32_dict :: "( 32 word)Ord_class " where " instance_Basic_classes_Ord_Num_int32_dict = ((| - compare_method = (genericCompare word_sless (op=)), + compare_method = (genericCompare word_sless (=)), isLess_method = word_sless, @@ -591,7 +590,7 @@ definition instance_Num_NumAbs_Num_int32_dict :: "( 32 word)NumAbs_class " whe definition instance_Num_NumAdd_Num_int32_dict :: "( 32 word)NumAdd_class " where " instance_Num_NumAdd_Num_int32_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val int32Minus : int32 -> int32 -> int32*) @@ -599,7 +598,7 @@ definition instance_Num_NumAdd_Num_int32_dict :: "( 32 word)NumAdd_class " whe definition instance_Num_NumMinus_Num_int32_dict :: "( 32 word)NumMinus_class " where " instance_Num_NumMinus_Num_int32_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val int32Succ : int32 -> int32*) @@ -622,7 +621,7 @@ definition instance_Num_NumPred_Num_int32_dict :: "( 32 word)NumPred_class " w definition instance_Num_NumMult_Num_int32_dict :: "( 32 word)NumMult_class " where " instance_Num_NumMult_Num_int32_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" @@ -631,7 +630,7 @@ definition instance_Num_NumMult_Num_int32_dict :: "( 32 word)NumMult_class " w definition instance_Num_NumPow_Num_int32_dict :: "( 32 word)NumPow_class " where " instance_Num_NumPow_Num_int32_dict = ((| - numPow_method = (op^)|) )" + numPow_method = (^)|) )" (*val int32Div : int32 -> int32 -> int32*) @@ -639,13 +638,13 @@ definition instance_Num_NumPow_Num_int32_dict :: "( 32 word)NumPow_class " whe definition instance_Num_NumIntegerDivision_Num_int32_dict :: "( 32 word)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_int32_dict = ((| - div_method = (op div)|) )" + div_method = (div)|) )" definition instance_Num_NumDivision_Num_int32_dict :: "( 32 word)NumDivision_class " where " instance_Num_NumDivision_Num_int32_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val int32Mod : int32 -> int32 -> int32*) @@ -653,7 +652,7 @@ definition instance_Num_NumDivision_Num_int32_dict :: "( 32 word)NumDivision_cl definition instance_Num_NumRemainder_Num_int32_dict :: "( 32 word)NumRemainder_class " where " instance_Num_NumRemainder_Num_int32_dict = ((| - mod_method = (op mod)|) )" + mod_method = (mod)|) )" (*val int32Min : int32 -> int32 -> int32*) @@ -687,7 +686,7 @@ definition instance_Basic_classes_OrdMaxMin_Num_int32_dict :: "( 32 word)OrdMax definition instance_Basic_classes_Ord_Num_int64_dict :: "( 64 word)Ord_class " where " instance_Basic_classes_Ord_Num_int64_dict = ((| - compare_method = (genericCompare word_sless (op=)), + compare_method = (genericCompare word_sless (=)), isLess_method = word_sless, @@ -723,7 +722,7 @@ definition instance_Num_NumAbs_Num_int64_dict :: "( 64 word)NumAbs_class " whe definition instance_Num_NumAdd_Num_int64_dict :: "( 64 word)NumAdd_class " where " instance_Num_NumAdd_Num_int64_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val int64Minus : int64 -> int64 -> int64*) @@ -731,7 +730,7 @@ definition instance_Num_NumAdd_Num_int64_dict :: "( 64 word)NumAdd_class " whe definition instance_Num_NumMinus_Num_int64_dict :: "( 64 word)NumMinus_class " where " instance_Num_NumMinus_Num_int64_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val int64Succ : int64 -> int64*) @@ -754,7 +753,7 @@ definition instance_Num_NumPred_Num_int64_dict :: "( 64 word)NumPred_class " w definition instance_Num_NumMult_Num_int64_dict :: "( 64 word)NumMult_class " where " instance_Num_NumMult_Num_int64_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" @@ -763,7 +762,7 @@ definition instance_Num_NumMult_Num_int64_dict :: "( 64 word)NumMult_class " w definition instance_Num_NumPow_Num_int64_dict :: "( 64 word)NumPow_class " where " instance_Num_NumPow_Num_int64_dict = ((| - numPow_method = (op^)|) )" + numPow_method = (^)|) )" (*val int64Div : int64 -> int64 -> int64*) @@ -771,13 +770,13 @@ definition instance_Num_NumPow_Num_int64_dict :: "( 64 word)NumPow_class " whe definition instance_Num_NumIntegerDivision_Num_int64_dict :: "( 64 word)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_int64_dict = ((| - div_method = (op div)|) )" + div_method = (div)|) )" definition instance_Num_NumDivision_Num_int64_dict :: "( 64 word)NumDivision_class " where " instance_Num_NumDivision_Num_int64_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val int64Mod : int64 -> int64 -> int64*) @@ -785,7 +784,7 @@ definition instance_Num_NumDivision_Num_int64_dict :: "( 64 word)NumDivision_cl definition instance_Num_NumRemainder_Num_int64_dict :: "( 64 word)NumRemainder_class " where " instance_Num_NumRemainder_Num_int64_dict = ((| - mod_method = (op mod)|) )" + mod_method = (mod)|) )" (*val int64Min : int64 -> int64 -> int64*) @@ -821,15 +820,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_int64_dict :: "( 64 word)OrdMax definition instance_Basic_classes_Ord_Num_integer_dict :: "(int)Ord_class " where " instance_Basic_classes_Ord_Num_integer_dict = ((| - compare_method = (genericCompare (op<) (op=)), + compare_method = (genericCompare (<) (=)), - isLess_method = (op<), + isLess_method = (<), - isLessEqual_method = (op \<le>), + isLessEqual_method = (\<le>), - isGreater_method = (op>), + isGreater_method = (>), - isGreaterEqual_method = (op \<ge>)|) )" + isGreaterEqual_method = (\<ge>)|) )" (*val integerNegate : integer -> integer*) @@ -853,7 +852,7 @@ definition instance_Num_NumAbs_Num_integer_dict :: "(int)NumAbs_class " where definition instance_Num_NumAdd_Num_integer_dict :: "(int)NumAdd_class " where " instance_Num_NumAdd_Num_integer_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val integerMinus : integer -> integer -> integer*) @@ -861,7 +860,7 @@ definition instance_Num_NumAdd_Num_integer_dict :: "(int)NumAdd_class " where definition instance_Num_NumMinus_Num_integer_dict :: "(int)NumMinus_class " where " instance_Num_NumMinus_Num_integer_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val integerSucc : integer -> integer*) @@ -883,7 +882,7 @@ definition instance_Num_NumPred_Num_integer_dict :: "(int)NumPred_class " wher definition instance_Num_NumMult_Num_integer_dict :: "(int)NumMult_class " where " instance_Num_NumMult_Num_integer_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" @@ -892,7 +891,7 @@ definition instance_Num_NumMult_Num_integer_dict :: "(int)NumMult_class " wher definition instance_Num_NumPow_Num_integer_dict :: "(int)NumPow_class " where " instance_Num_NumPow_Num_integer_dict = ((| - numPow_method = (op^)|) )" + numPow_method = (^)|) )" (*val integerDiv : integer -> integer -> integer*) @@ -900,13 +899,13 @@ definition instance_Num_NumPow_Num_integer_dict :: "(int)NumPow_class " where definition instance_Num_NumIntegerDivision_Num_integer_dict :: "(int)NumIntegerDivision_class " where " instance_Num_NumIntegerDivision_Num_integer_dict = ((| - div_method = (op div)|) )" + div_method = (div)|) )" definition instance_Num_NumDivision_Num_integer_dict :: "(int)NumDivision_class " where " instance_Num_NumDivision_Num_integer_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val integerMod : integer -> integer -> integer*) @@ -914,7 +913,7 @@ definition instance_Num_NumDivision_Num_integer_dict :: "(int)NumDivision_class definition instance_Num_NumRemainder_Num_integer_dict :: "(int)NumRemainder_class " where " instance_Num_NumRemainder_Num_integer_dict = ((| - mod_method = (op mod)|) )" + mod_method = (mod)|) )" (*val integerMin : integer -> integer -> integer*) @@ -951,15 +950,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_integer_dict :: "(int)OrdMaxMin definition instance_Basic_classes_Ord_Num_rational_dict :: "(rat)Ord_class " where " instance_Basic_classes_Ord_Num_rational_dict = ((| - compare_method = (genericCompare (op<) (op=)), + compare_method = (genericCompare (<) (=)), - isLess_method = (op<), + isLess_method = (<), - isLessEqual_method = (op \<le>), + isLessEqual_method = (\<le>), - isGreater_method = (op>), + isGreater_method = (>), - isGreaterEqual_method = (op \<ge>)|) )" + isGreaterEqual_method = (\<ge>)|) )" (*val rationalAdd : rational -> rational -> rational*) @@ -967,7 +966,7 @@ definition instance_Basic_classes_Ord_Num_rational_dict :: "(rat)Ord_class " w definition instance_Num_NumAdd_Num_rational_dict :: "(rat)NumAdd_class " where " instance_Num_NumAdd_Num_rational_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val rationalMinus : rational -> rational -> rational*) @@ -975,7 +974,7 @@ definition instance_Num_NumAdd_Num_rational_dict :: "(rat)NumAdd_class " where definition instance_Num_NumMinus_Num_rational_dict :: "(rat)NumMinus_class " where " instance_Num_NumMinus_Num_rational_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val rationalNegate : rational -> rational*) @@ -1013,7 +1012,7 @@ definition instance_Num_NumPred_Num_rational_dict :: "(rat)NumPred_class " whe definition instance_Num_NumMult_Num_rational_dict :: "(rat)NumMult_class " where " instance_Num_NumMult_Num_rational_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" (*val rationalDiv : rational -> rational -> rational*) @@ -1021,7 +1020,7 @@ definition instance_Num_NumMult_Num_rational_dict :: "(rat)NumMult_class " whe definition instance_Num_NumDivision_Num_rational_dict :: "(rat)NumDivision_class " where " instance_Num_NumDivision_Num_rational_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val rationalFromFrac : int -> int -> rational*) @@ -1078,15 +1077,15 @@ definition instance_Basic_classes_OrdMaxMin_Num_rational_dict :: "(rat)OrdMaxMi definition instance_Basic_classes_Ord_Num_real_dict :: "(real)Ord_class " where " instance_Basic_classes_Ord_Num_real_dict = ((| - compare_method = (genericCompare (op<) (op=)), + compare_method = (genericCompare (<) (=)), - isLess_method = (op<), + isLess_method = (<), - isLessEqual_method = (op \<le>), + isLessEqual_method = (\<le>), - isGreater_method = (op>), + isGreater_method = (>), - isGreaterEqual_method = (op \<ge>)|) )" + isGreaterEqual_method = (\<ge>)|) )" (*val realAdd : real -> real -> real*) @@ -1094,7 +1093,7 @@ definition instance_Basic_classes_Ord_Num_real_dict :: "(real)Ord_class " wher definition instance_Num_NumAdd_Num_real_dict :: "(real)NumAdd_class " where " instance_Num_NumAdd_Num_real_dict = ((| - numAdd_method = (op+)|) )" + numAdd_method = (+)|) )" (*val realMinus : real -> real -> real*) @@ -1102,7 +1101,7 @@ definition instance_Num_NumAdd_Num_real_dict :: "(real)NumAdd_class " where definition instance_Num_NumMinus_Num_real_dict :: "(real)NumMinus_class " where " instance_Num_NumMinus_Num_real_dict = ((| - numMinus_method = (op-)|) )" + numMinus_method = (-)|) )" (*val realNegate : real -> real*) @@ -1140,7 +1139,7 @@ definition instance_Num_NumPred_Num_real_dict :: "(real)NumPred_class " where definition instance_Num_NumMult_Num_real_dict :: "(real)NumMult_class " where " instance_Num_NumMult_Num_real_dict = ((| - numMult_method = (op*)|) )" + numMult_method = ( * )|) )" (*val realDiv : real -> real -> real*) @@ -1148,7 +1147,7 @@ definition instance_Num_NumMult_Num_real_dict :: "(real)NumMult_class " where definition instance_Num_NumDivision_Num_real_dict :: "(real)NumDivision_class " where " instance_Num_NumDivision_Num_real_dict = ((| - numDivision_method = (op div)|) )" + numDivision_method = (div)|) )" (*val realFromFrac : integer -> integer -> real*) |