afford full test, with slightly improved scheduling order;
authorwenzelm
Sat Dec 20 00:05:20 2014 +0100 (2014-12-20)
changeset 59162dca5594761f2
parent 59161 5a13df748fac
child 59163 857a600f0c94
afford full test, with slightly improved scheduling order;
src/HOL/Nominal/Examples/Nominal_Examples.thy
src/HOL/Nominal/Examples/Nominal_Examples_Base.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Nominal/Examples/Nominal_Examples.thy	Fri Dec 19 23:33:08 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,9 +0,0 @@
     1.4 -(*  Author:  Christian Urban TU Muenchen *)
     1.5 -
     1.6 -section {* Various examples involving nominal datatypes. *}
     1.7 -
     1.8 -theory Nominal_Examples
     1.9 -imports Nominal_Examples_Base Class3
    1.10 -begin
    1.11 -
    1.12 -end
     2.1 --- a/src/HOL/Nominal/Examples/Nominal_Examples_Base.thy	Fri Dec 19 23:33:08 2014 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,27 +0,0 @@
     2.4 -(*  Author:  Christian Urban TU Muenchen *)
     2.5 -
     2.6 -section {* Various examples involving nominal datatypes. *}
     2.7 -
     2.8 -theory Nominal_Examples_Base
     2.9 -imports
    2.10 -  CK_Machine
    2.11 -  CR
    2.12 -  CR_Takahashi
    2.13 -  Compile
    2.14 -  Contexts
    2.15 -  Crary
    2.16 -  Fsub
    2.17 -  Height
    2.18 -  Lambda_mu
    2.19 -  LocalWeakening
    2.20 -  Pattern
    2.21 -  SN
    2.22 -  SOS
    2.23 -  Standardization
    2.24 -  Support
    2.25 -  Type_Preservation
    2.26 -  W
    2.27 -  Weakening
    2.28 -begin
    2.29 -
    2.30 -end
     3.1 --- a/src/HOL/ROOT	Fri Dec 19 23:33:08 2014 +0100
     3.2 +++ b/src/HOL/ROOT	Sat Dec 20 00:05:20 2014 +0100
     3.3 @@ -725,9 +725,26 @@
     3.4  session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
     3.5    options [condition = ML_SYSTEM_POLYML, document = false]
     3.6    theories
     3.7 -    Nominal_Examples_Base
     3.8 -  theories [condition = ISABELLE_FULL_TEST]
     3.9 -    Nominal_Examples
    3.10 +    Class3
    3.11 +    CK_Machine
    3.12 +    Compile
    3.13 +    Contexts
    3.14 +    Crary
    3.15 +    CR_Takahashi
    3.16 +    CR
    3.17 +    Fsub
    3.18 +    Height
    3.19 +    Lambda_mu
    3.20 +    Lam_Funs
    3.21 +    LocalWeakening
    3.22 +    Pattern
    3.23 +    SN
    3.24 +    SOS
    3.25 +    Standardization
    3.26 +    Support
    3.27 +    Type_Preservation
    3.28 +    Weakening
    3.29 +    W
    3.30    theories [quick_and_dirty]
    3.31      VC_Condition
    3.32