author | wenzelm |
Sun, 22 Jul 2001 21:30:05 +0200 | |
changeset 11438 | 3d9222b80989 |
parent 11437 | 2338bce575ae |
child 11439 | 9aaab1a160a5 |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Fri Jul 20 22:02:45 2001 +0200 +++ b/src/HOL/HOL.thy Sun Jul 22 21:30:05 2001 +0200 @@ -211,6 +211,8 @@ use "HOL_lemmas.ML" +declare trans [trans] (*overridden in theory Calculation*) + lemma atomize_all: "(!!x. P x) == Trueprop (ALL x. P x)" proof (rule equal_intr_rule) assume "!!x. P x"