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

     8 imports Main Infinite_Set

     8 imports Main Infinite_Set

     9 begin

    10 begin

    10 

    11 

    11 section {* Atoms and Sorts *}

    12 section {* Atoms and Sorts *}

    12 

    13 

    13 text {* A simple implementation for atom_sorts is strings. *}

    14 text {* A simple implementation for atom_sorts is strings. *}

  1057     unfolding fresh_def

  1058     unfolding fresh_def

  1058     using supp_fun_app b

  1059     using supp_fun_app b

  1059     by auto

  1060     by auto

  1060 qed

  1061 qed

  1061 

  1062