src/HOL/Import/HOL4Compat.thy
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 15003 6145dd7538d7
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      HOL/Import/HOL4Compat.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9  theory HOL4Compat = HOL4Setup + Divides + Primes + Real:
    1.10  
    1.11  lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"