src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
changeset 39198 f967a16dfcdd
parent 37008 8da3b51726ac
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  lemma [code_pred_inline]:
     1.6    "max = max_nat"
     1.7 -by (simp add: expand_fun_eq max_def max_nat_def)
     1.8 +by (simp add: ext_iff max_def max_nat_def)
     1.9  
    1.10  definition
    1.11    "max_of_my_Suc x = max x (Suc x)"