src/HOL/Nominal/Examples/Weakening.thy
changeset 18653 7a00c80400b1
parent 18354 715d6df89fcc
child 18654 94782c7c4247
equal deleted inserted replaced
18652:3930a060d71b 18653:7a00c80400b1
    40   fixes   pi:: "name prm"
    40   fixes   pi:: "name prm"
    41   assumes a: "valid \<Gamma>"
    41   assumes a: "valid \<Gamma>"
    42   shows   "valid (pi\<bullet>\<Gamma>)"
    42   shows   "valid (pi\<bullet>\<Gamma>)"
    43 using a
    43 using a
    44 apply(induct)
    44 apply(induct)
    45 apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
    45 apply(auto simp add: fresh_eqvt)
    46 done
    46 done
    47 
    47 
    48 (* typing judgements *)
    48 (* typing judgements *)
    49 consts
    49 consts
    50   typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
    50   typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set"