src/HOL/ROOT
changeset 59162 dca5594761f2
parent 59144 c9b75c03de3c
child 59190 3a594fd13ca4
     1.1 --- a/src/HOL/ROOT	Fri Dec 19 23:33:08 2014 +0100
     1.2 +++ b/src/HOL/ROOT	Sat Dec 20 00:05:20 2014 +0100
     1.3 @@ -725,9 +725,26 @@
     1.4  session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
     1.5    options [condition = ML_SYSTEM_POLYML, document = false]
     1.6    theories
     1.7 -    Nominal_Examples_Base
     1.8 -  theories [condition = ISABELLE_FULL_TEST]
     1.9 -    Nominal_Examples
    1.10 +    Class3
    1.11 +    CK_Machine
    1.12 +    Compile
    1.13 +    Contexts
    1.14 +    Crary
    1.15 +    CR_Takahashi
    1.16 +    CR
    1.17 +    Fsub
    1.18 +    Height
    1.19 +    Lambda_mu
    1.20 +    Lam_Funs
    1.21 +    LocalWeakening
    1.22 +    Pattern
    1.23 +    SN
    1.24 +    SOS
    1.25 +    Standardization
    1.26 +    Support
    1.27 +    Type_Preservation
    1.28 +    Weakening
    1.29 +    W
    1.30    theories [quick_and_dirty]
    1.31      VC_Condition
    1.32