3 

     3 

     4     Basic definitions and lemma infrastructure for 

     4     Basic definitions and lemma infrastructure for 

     5     Nominal Isabelle. 

     5     Nominal Isabelle. 

     6 *)

     6 *)

     7 theory Nominal2_Base

     7 theory Nominal2_Base

     9         "~~/src/HOL/Quotient_Examples/FSet"

    10         "~~/src/HOL/Quotient_Examples/FSet"

    10 uses ("nominal_library.ML")

    11 uses ("nominal_library.ML")

    11      ("nominal_atoms.ML")

    12      ("nominal_atoms.ML")

    12 begin

    13 begin

    13 

    14 

   684 instance unit :: pure

   685 instance unit :: pure

   685 proof qed (rule permute_unit_def)

   686 proof qed (rule permute_unit_def)

   686 

   687 

   687 instance bool :: pure

   688 instance bool :: pure

   688 proof qed (rule permute_bool_def)

   689 proof qed (rule permute_bool_def)

   689 

   691 

   690 text {* Other type constructors preserve purity. *}

   692 text {* Other type constructors preserve purity. *}

   691 

   693 

   692 instance "fun" :: (pure, pure) pure

   694 instance "fun" :: (pure, pure) pure

   693 by default (simp add: permute_fun_def permute_pure)

   695 by default (simp add: permute_fun_def permute_pure)