Nominal/Test.thy
changeset 1342 2b98012307f7
parent 1341 c25f797c7e6e
child 1355 7b0c6d07a24e
equal deleted inserted replaced
1341:c25f797c7e6e 1342:2b98012307f7
   146 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
   146 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
   147 (*thm lam_bp_induct
   147 (*thm lam_bp_induct
   148 thm lam_bp_perm
   148 thm lam_bp_perm
   149 thm lam_bp_fv
   149 thm lam_bp_fv
   150 thm lam_bp_bn
   150 thm lam_bp_bn
   151 thm lam_bp_inject*)
   151 thm lam_bp_inject
       
   152 thm lam_bp_distinct*)
   152 
   153 
   153 text {* example 2 *}
   154 text {* example 2 *}
   154 
   155 
   155 nominal_datatype trm' =
   156 nominal_datatype trm' =
   156   Var "name"
   157   Var "name"