src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 39919 9f6503aaa77d
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Sep 13 11:13:15 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: ext_iff max_def max_nat_def)
     1.8 +by (simp add: fun_eq_iff max_def max_nat_def)
     1.9  
    1.10  definition
    1.11    "max_of_my_Suc x = max x (Suc x)"