declare trans [trans] (*overridden in theory Calculation*);
authorwenzelm
Sun Jul 22 21:30:05 2001 +0200 (2001-07-22)
changeset 114383d9222b80989
parent 11437 2338bce575ae
child 11439 9aaab1a160a5
declare trans [trans] (*overridden in theory Calculation*);
src/HOL/HOL.thy
     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"