# HG changeset patch
# User haftmann
# Date 1237792462 -3600
# Node ID 53e1b1641f09d2b4ec4da70cbb231872d4f9b815
# Parent  40a1865ab1221eba6190356fb47b4f3ada9606d5
more canonical import, syntax fix

diff -r 40a1865ab122 -r 53e1b1641f09 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Fri Mar 20 11:26:59 2009 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 08:14:22 2009 +0100
@@ -1,11 +1,14 @@
 (*  Title:      HOL/Import/HOL4Compat.thy
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
+theory HOL4Compat
+imports HOL4Setup Complex_Main Primes ContNotDenum
 begin
 
+no_notation differentiable (infixl "differentiable" 60)
+no_notation sums (infixr "sums" 80)
+
 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
   by auto
 
@@ -22,7 +25,7 @@
 lemmas [hol4rew] = ONE_ONE_rew
 
 lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
-  by simp;
+  by simp
 
 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
   by safe