src/HOL/ROOT
changeset 64551 79e9587dbcca
parent 64431 ae53f4d901a3
child 64555 628b271c5b8b
     1.1 --- a/src/HOL/ROOT	Sun Oct 30 13:15:14 2016 +0100
     1.2 +++ b/src/HOL/ROOT	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -38,7 +38,6 @@
     1.4      Predicate_Compile_Quickcheck
     1.5      Prefix_Order
     1.6      Rewrite
     1.7 -    Types_To_Sets
     1.8      (*conflicting type class instantiations*)
     1.9      List_lexord
    1.10      Sublist_Order
    1.11 @@ -1021,6 +1020,17 @@
    1.12    theories [condition = ISABELLE_SWIPL, quick_and_dirty]
    1.13      Reg_Exp_Example
    1.14  
    1.15 +session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
    1.16 +  description {*
    1.17 +    Experimental extension of Higher-Order Logic to allow translation of types to sets.
    1.18 +  *}
    1.19 +  options [document = false]
    1.20 +  theories
    1.21 +    Types_To_Sets
    1.22 +    "Examples/Prerequisites"
    1.23 +    "Examples/Finite"
    1.24 +    "Examples/T2_Spaces"
    1.25 +
    1.26  session HOLCF (main timing) in HOLCF = HOL +
    1.27    description {*
    1.28      Author:     Franz Regensburger