src/HOL/Nominal/Examples/Class3.thy
changeset 61943 7fba644ed827
parent 55417 01fbfb60c33e
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -2265,7 +2265,7 @@
     1.4  by (induct rule: SNa.induct) (blast)
     1.5  
     1.6  lemma wf_SNa_restricted:
     1.7 -  shows "wf (A_Redu_set \<inter> (UNIV <*> SNa_set))"
     1.8 +  shows "wf (A_Redu_set \<inter> (UNIV \<times> SNa_set))"
     1.9  apply(unfold wf_def)
    1.10  apply(intro strip)
    1.11  apply(case_tac "SNa x")
    1.12 @@ -2280,7 +2280,7 @@
    1.13  done
    1.14  
    1.15  definition SNa_Redu :: "(trm \<times> trm) set" where
    1.16 -  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV <*> SNa_set)"
    1.17 +  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV \<times> SNa_set)"
    1.18  
    1.19  lemma wf_SNa_Redu:
    1.20    shows "wf SNa_Redu"