src/HOL/Import/HOL4Compat.thy
 changeset 30660 53e1b1641f09 parent 30235 58d147683393 child 30952 7ab2716dd93b
```     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Fri Mar 20 11:26:59 2009 +0100
1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 08:14:22 2009 +0100
1.3 @@ -1,11 +1,14 @@
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 imports HOL4Setup Divides Primes Real ContNotDenum
1.10 +theory HOL4Compat
1.11 +imports HOL4Setup Complex_Main Primes ContNotDenum
1.12  begin
1.13
1.14 +no_notation differentiable (infixl "differentiable" 60)
1.15 +no_notation sums (infixr "sums" 80)
1.16 +
1.17  lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
1.18    by auto
1.19
1.20 @@ -22,7 +25,7 @@
1.21  lemmas [hol4rew] = ONE_ONE_rew
1.22
1.23  lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
1.24 -  by simp;
1.25 +  by simp
1.26
1.27  lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
1.28    by safe
```