run larger nominal examples only 'ISABELLE_FULL_TEST'
authorblanchet
Fri Sep 12 16:42:36 2014 +0200 (2014-09-12)
changeset 58329a31404ec7414
parent 58328 086193f231ea
child 58330 a016c42d136d
run larger nominal examples only 'ISABELLE_FULL_TEST'
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 Sep 12 13:50:55 2014 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy	Fri Sep 12 16:42:36 2014 +0200
     1.3 @@ -3,26 +3,7 @@
     1.4  header {* Various examples involving nominal datatypes. *}
     1.5  
     1.6  theory Nominal_Examples
     1.7 -imports
     1.8 -  CK_Machine
     1.9 -  CR
    1.10 -  CR_Takahashi
    1.11 -  Class3
    1.12 -  Compile
    1.13 -  Contexts
    1.14 -  Crary
    1.15 -  Fsub
    1.16 -  Height
    1.17 -  Lambda_mu
    1.18 -  LocalWeakening
    1.19 -  Pattern
    1.20 -  SN
    1.21 -  SOS
    1.22 -  Standardization
    1.23 -  Support
    1.24 -  Type_Preservation
    1.25 -  W
    1.26 -  Weakening
    1.27 +imports Nominal_Examples_Base Class3
    1.28  begin
    1.29  
    1.30  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Nominal/Examples/Nominal_Examples_Base.thy	Fri Sep 12 16:42:36 2014 +0200
     2.3 @@ -0,0 +1,27 @@
     2.4 +(*  Author:  Christian Urban TU Muenchen *)
     2.5 +
     2.6 +header {* 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 Sep 12 13:50:55 2014 +0200
     3.2 +++ b/src/HOL/ROOT	Fri Sep 12 16:42:36 2014 +0200
     3.3 @@ -716,8 +716,12 @@
     3.4  
     3.5  session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
     3.6    options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
     3.7 -  theories Nominal_Examples
     3.8 -  theories [quick_and_dirty] VC_Condition
     3.9 +  theories
    3.10 +    Nominal_Examples_Base
    3.11 +  theories [condition = ISABELLE_FULL_TEST]
    3.12 +    Nominal_Examples
    3.13 +  theories [quick_and_dirty]
    3.14 +    VC_Condition
    3.15  
    3.16  session "HOL-Cardinals" in Cardinals = HOL +
    3.17    description {*