Nominal/Perm.thy
author Christian Urban <urbanc@in.tum.de>
Thu, 22 Jul 2010 08:30:50 +0200
changeset 2378 2f13fe48c877
parent 2346 4c5881455923
permissions -rw-r--r--
updated to new Isabelle; made FSet more "quiet"

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