summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Hilbert_Classical.thy

changeset 11635 | fd242f857508 |

parent 11591 | 4b171ad4ff65 |

child 14981 | e73f8140af78 |

--- a/src/HOL/ex/Hilbert_Classical.thy Fri Sep 28 19:24:25 2001 +0200 +++ b/src/HOL/ex/Hilbert_Classical.thy Fri Sep 28 20:08:05 2001 +0200 @@ -52,8 +52,7 @@ hence "Eps ?P = Eps ?Q" by (rule arg_cong) also note P also note Q - finally have "False = True" . - thus False by (rule False_neq_True) + finally show False by (rule False_neq_True) qed have "\<not> A" proof