src/HOL/ROOT

     Finite_Lattice
     Code_Char_chr
     Code_Char_ord
     Product_Lexorder
     Product_Order
-    Code_Integer
-    Efficient_Nat
     (* Code_Prolog  FIXME cf. 76965c356d2a *)
     Code_Real_Approx_By_Float
     Code_Target_Numeral
     IArray
     Refute

   description {* *}
   options [document_graph, print_mode = "iff,no_brackets"]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Monad_Syntax"
-    "~~/src/HOL/Library/Code_Natural"
     "~~/src/HOL/Library/LaTeXsugar"
   theories Imperative_HOL_ex
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Decision_Procs" in Decision_Procs = HOL +

 
 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   description {* Examples for program extraction in Higher-Order Logic *}
   options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   theories [document = false]
-    "~~/src/HOL/Library/Efficient_Nat"
+    "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Number_Theory/Primes"
     "~~/src/HOL/Number_Theory/UniqueFactorization"
     "~~/src/HOL/Library/State_Monad"
   theories

   files "document/root.bib" "document/root.tex"
 
 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
   theories [document = false]
-    "~~/src/HOL/Library/Code_Integer"
+    "~~/src/HOL/Library/Code_Target_Int"
   theories
     Eta
     StrongNorm
     Standardization
     WeakNorm