Nominal/Perm.thy
author Christian Urban <urbanc@in.tum.de>
Sun, 18 Jul 2010 19:07:05 +0100
changeset 2371 86c73a06ba4b
parent 2346 4c5881455923
permissions -rw-r--r--
minor things on the paper

theory Perm
imports 
  "../Nominal-General/Nominal2_Base"
  "../Nominal-General/Nominal2_Atoms" 
  "../Nominal-General/Nominal2_Eqvt" 
  "Nominal2_FSet"
  "Abs"
uses ("nominal_dt_rawperm.ML")
     ("nominal_dt_rawfuns.ML")
     ("nominal_dt_alpha.ML")
     ("nominal_dt_quot.ML")
begin

use "nominal_dt_rawperm.ML"
ML {* open Nominal_Dt_RawPerm *}

use "nominal_dt_rawfuns.ML"
ML {* open Nominal_Dt_RawFuns *}

use "nominal_dt_alpha.ML"
ML {* open Nominal_Dt_Alpha *}

use "nominal_dt_quot.ML"
ML {* open Nominal_Dt_Quot *}


end