src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 47433 07f4bf913230
parent 47108 2a1953f0d20d
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -1027,8 +1027,8 @@
     1.4    (o * o => bool) => i * i => bool) [inductify] converse .
     1.5  
     1.6  thm converse.equation
     1.7 -code_pred [inductify] rel_comp .
     1.8 -thm rel_comp.equation
     1.9 +code_pred [inductify] relcomp .
    1.10 +thm relcomp.equation
    1.11  code_pred [inductify] Image .
    1.12  thm Image.equation
    1.13  declare singleton_iff[code_pred_inline]