more canonical import, syntax fix
authorhaftmann
Mon Mar 23 08:14:22 2009 +0100 (2009-03-23)
changeset 3066053e1b1641f09
parent 30606 40a1865ab122
child 30661 54858c8ad226
more canonical import, syntax fix
src/HOL/Import/HOL4Compat.thy
     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