summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Nominal/Nominal.thy

changeset 41550 | efa734d9b221 |

parent 41413 | 64cd30d6b0b8 |

child 41562 | 90fb3d7474df |

1.1 --- a/src/HOL/Nominal/Nominal.thy Fri Jan 14 15:43:04 2011 +0100 1.2 +++ b/src/HOL/Nominal/Nominal.thy Fri Jan 14 15:44:47 2011 +0100 1.3 @@ -785,7 +785,7 @@ 1.4 hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:) 1.5 then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force 1.6 then have "c\<notin>A" by simp 1.7 - then show ?thesis using prems by simp 1.8 + then show ?thesis .. 1.9 qed 1.10 1.11 text {* there always exists a fresh name for an object with finite support *}