Nominal/Perm.thy
author Christian Urban <urbanc@in.tum.de>
Sun, 22 Aug 2010 12:36:53 +0800
changeset 2429 b29eb13d3f9d
parent 2346 4c5881455923
permissions -rw-r--r--
merged

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