src/HOL/Import/HOLLightCompat.thy
changeset 35416 d8d7d1b785af
parent 19064 bf19cc5a7899
child 41589 bbd861837ebc
--- a/src/HOL/Import/HOLLightCompat.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Import/HOLLightCompat.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -30,8 +30,7 @@
     by simp
 qed
 
-constdefs
-   Pred :: "nat \<Rightarrow> nat"
+definition Pred :: "nat \<Rightarrow> nat" where
    "Pred n \<equiv> n - (Suc 0)"
 
 lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
@@ -84,8 +83,7 @@
   apply auto
   done
 
-constdefs
-  NUMERAL_BIT0 :: "nat \<Rightarrow> nat"
+definition NUMERAL_BIT0 :: "nat \<Rightarrow> nat" where
   "NUMERAL_BIT0 n \<equiv> n + n"
 
 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"