src/HOL/ROOT
changeset 51143 0a2371e7ced3
parent 51115 7dbd6832a689
child 51160 599ff65b85e2
     1.1 --- a/src/HOL/ROOT	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/ROOT	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -28,8 +28,6 @@
     1.4      Code_Char_ord
     1.5      Product_Lexorder
     1.6      Product_Order
     1.7 -    Code_Integer
     1.8 -    Efficient_Nat
     1.9      (* Code_Prolog  FIXME cf. 76965c356d2a *)
    1.10      Code_Real_Approx_By_Float
    1.11      Code_Target_Numeral
    1.12 @@ -282,7 +280,6 @@
    1.13    theories [document = false]
    1.14      "~~/src/HOL/Library/Countable"
    1.15      "~~/src/HOL/Library/Monad_Syntax"
    1.16 -    "~~/src/HOL/Library/Code_Natural"
    1.17      "~~/src/HOL/Library/LaTeXsugar"
    1.18    theories Imperative_HOL_ex
    1.19    files "document/root.bib" "document/root.tex"
    1.20 @@ -299,7 +296,7 @@
    1.21    description {* Examples for program extraction in Higher-Order Logic *}
    1.22    options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
    1.23    theories [document = false]
    1.24 -    "~~/src/HOL/Library/Efficient_Nat"
    1.25 +    "~~/src/HOL/Library/Code_Target_Numeral"
    1.26      "~~/src/HOL/Library/Monad_Syntax"
    1.27      "~~/src/HOL/Number_Theory/Primes"
    1.28      "~~/src/HOL/Number_Theory/UniqueFactorization"
    1.29 @@ -315,7 +312,7 @@
    1.30  session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
    1.31    options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
    1.32    theories [document = false]
    1.33 -    "~~/src/HOL/Library/Code_Integer"
    1.34 +    "~~/src/HOL/Library/Code_Target_Int"
    1.35    theories
    1.36      Eta
    1.37      StrongNorm