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