Nominal/Perm.thy
author Christian Urban <urbanc@in.tum.de>
Tue, 17 Aug 2010 17:52:25 +0800
changeset 2407 49ab06c0ca64
parent 2346 4c5881455923
permissions -rw-r--r--
improved code

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