diff options
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_num.thy')
| -rw-r--r-- | snapshots/isabelle/lib/lem/Lem_num.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_num.thy b/snapshots/isabelle/lib/lem/Lem_num.thy index 0d7a72ea..ddbdd533 100644 --- a/snapshots/isabelle/lib/lem/Lem_num.thy +++ b/snapshots/isabelle/lib/lem/Lem_num.thy @@ -16,8 +16,8 @@ begin (*open import Bool Basic_classes*) (*open import {isabelle} `~~/src/HOL/Word/Word` `Real` `~~/src/HOL/NthRoot`*) -(*open import {hol} `integerTheory` `intReduce` `wordsTheory` `wordsLib` `ratTheory` `realTheory` `intrealTheory`*) -(*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.Reals.ROrderedType` `Coq.Reals.Rbase` `Coq.Reals.Rfunctions`*) +(*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`*) (*class inline ( Numeral 'a ) val fromNumeral : numeral -> 'a |