src/HOL/Import/HOLLightCompat.thy
changeset 35416 d8d7d1b785af
parent 19064 bf19cc5a7899
child 41589 bbd861837ebc
     1.1 --- a/src/HOL/Import/HOLLightCompat.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Import/HOLLightCompat.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -30,8 +30,7 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 -constdefs
     1.8 -   Pred :: "nat \<Rightarrow> nat"
     1.9 +definition Pred :: "nat \<Rightarrow> nat" where
    1.10     "Pred n \<equiv> n - (Suc 0)"
    1.11  
    1.12  lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
    1.13 @@ -84,8 +83,7 @@
    1.14    apply auto
    1.15    done
    1.16  
    1.17 -constdefs
    1.18 -  NUMERAL_BIT0 :: "nat \<Rightarrow> nat"
    1.19 +definition NUMERAL_BIT0 :: "nat \<Rightarrow> nat" where
    1.20    "NUMERAL_BIT0 n \<equiv> n + n"
    1.21  
    1.22  lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"