added session theory for Nominal_Examples
authorhaftmann
Mon Sep 21 16:01:30 2009 +0200 (2009-09-21)
changeset 3263537e32f8aa696
parent 32634 9b19cbb0af28
child 32636 55a0be42327c
added session theory for Nominal_Examples
src/HOL/Nominal/Examples/Nominal_Examples.thy
src/HOL/Nominal/Examples/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy	Mon Sep 21 16:01:30 2009 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(*  Author:  Christian Urban TU Muenchen *)
     1.5 +
     1.6 +header {* Various examples involving nominal datatypes. *}
     1.7 +
     1.8 +theory Nominal_Examples
     1.9 +imports
    1.10 +  CR
    1.11 +  CR_Takahashi
    1.12 +  Class
    1.13 +  Compile
    1.14 +  Fsub
    1.15 +  Height
    1.16 +  Lambda_mu
    1.17 +  SN
    1.18 +  Weakening
    1.19 +  Crary
    1.20 +  SOS
    1.21 +  LocalWeakening
    1.22 +  Support
    1.23 +  Contexts
    1.24 +  Standardization
    1.25 +  W
    1.26 +begin
    1.27 +
    1.28 +end
     2.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Mon Sep 21 16:00:53 2009 +0200
     2.2 +++ b/src/HOL/Nominal/Examples/ROOT.ML	Mon Sep 21 16:01:30 2009 +0200
     2.3 @@ -1,27 +1,4 @@
     2.4 -(*  Title:      HOL/Nominal/Examples/ROOT.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Christian Urban, TU Muenchen
     2.7 -
     2.8 -Various examples involving nominal datatypes.
     2.9 -*)
    2.10  
    2.11 -use_thys [
    2.12 -  "CR",
    2.13 -  "CR_Takahashi",
    2.14 -  "Class",
    2.15 -  "Compile",
    2.16 -  "Fsub",
    2.17 -  "Height",
    2.18 -  "Lambda_mu",
    2.19 -  "SN",
    2.20 -  "Weakening",
    2.21 -  "Crary",
    2.22 -  "SOS",
    2.23 -  "LocalWeakening",
    2.24 -  "Support",
    2.25 -  "Contexts",
    2.26 -  "Standardization",
    2.27 -  "W"
    2.28 -];
    2.29 +use_thy "Nominal_Examples";
    2.30  
    2.31 -setmp_noncritical quick_and_dirty true use_thy "VC_Condition";
    2.32 +setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)