src/HOL/HOL.thy
changeset 11438 3d9222b80989
parent 11432 8a203ae6efe3
child 11451 8abfb4f7bd02
     1.1 --- a/src/HOL/HOL.thy	Fri Jul 20 22:02:45 2001 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Jul 22 21:30:05 2001 +0200
     1.3 @@ -211,6 +211,8 @@
     1.4  
     1.5  use "HOL_lemmas.ML"
     1.6  
     1.7 +declare trans [trans]  (*overridden in theory Calculation*)
     1.8 +
     1.9  lemma atomize_all: "(!!x. P x) == Trueprop (ALL x. P x)"
    1.10  proof (rule equal_intr_rule)
    1.11    assume "!!x. P x"