src/HOL/Code_Generator.thy
changeset 21404 eb85850d3eb7
parent 21378 cedfce6fc725
child 21454 a1937c51ed88
     1.1 --- a/src/HOL/Code_Generator.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4  text {* lazy @{const If} *}
     1.5  
     1.6  definition
     1.7 -  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a"
     1.8 +  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
     1.9    "if_delayed b f g = (if b then f True else g False)"
    1.10  
    1.11  lemma [code func]: