src/HOL/ROOT
changeset 58372 bfd497f2f4c2
parent 58371 7f30ec82fe40
child 58385 9cbef70cff8e
     1.1 --- a/src/HOL/ROOT	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Thu Sep 18 16:47:40 2014 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    *}
     1.5    options [timeout = 5400, document = false]
     1.6    theories Proofs (*sequential change of global flag!*)
     1.7 -  theories Main
     1.8 +  theories "~~/src/HOL/Library/Old_Datatype"
     1.9    files
    1.10      "Tools/Quickcheck/Narrowing_Engine.hs"
    1.11      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    1.12 @@ -51,6 +51,7 @@
    1.13      RBT_Set
    1.14      (*legacy tools*)
    1.15      Refute
    1.16 +    Old_Datatype
    1.17      Old_Recdef
    1.18      Old_SMT
    1.19    theories [condition = ISABELLE_FULL_TEST]
    1.20 @@ -91,11 +92,13 @@
    1.21  
    1.22      PropLog proves the completeness of a formalization of propositional logic
    1.23      (see
    1.24 -    HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
    1.25 +    http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
    1.26  
    1.27      Exp demonstrates the use of iterated inductive definitions to reason about
    1.28      mutually recursive relations.
    1.29    *}
    1.30 +  theories [document = false]
    1.31 +    "~~/src/HOL/Library/Old_Datatype"
    1.32    theories [quick_and_dirty]
    1.33      Common_Patterns
    1.34    theories
    1.35 @@ -741,6 +744,7 @@
    1.36    *}
    1.37    options [document = false]
    1.38    theories
    1.39 +    "~~/src/HOL/Library/Old_Datatype"
    1.40      Compat
    1.41      Lambda_Term
    1.42      Process