Nominal/Perm.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 11 Aug 2010 16:23:50 +0800
changeset 2394 e2759a4dad4b
parent 2346 4c5881455923
permissions -rw-r--r--
updated to Isabelle 11 Aug

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