src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 44928 7ef6505bde7f
parent 44890 22f665a2e91c
child 45970 b6d0cff57d96
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -1017,7 +1017,7 @@
     1.4  code_pred [inductify] Image .
     1.5  thm Image.equation
     1.6  declare singleton_iff[code_pred_inline]
     1.7 -declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
     1.8 +declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]
     1.9  
    1.10  code_pred (expected_modes:
    1.11    (o => bool) => o => bool,