src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 39657 5e57675b7e40
parent 39655 8ad7fe9d6f0b
child 39762 02fb709ab3cb
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 23 14:50:18 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 23 17:22:44 2010 +0200
     1.3 @@ -1327,10 +1327,10 @@
     1.4  text {* The global introduction rules must be redeclared as introduction rules and then 
     1.5    one could invoke code_pred. *}
     1.6  
     1.7 -declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro]
     1.8 +declare A.hd_predicate_in_locale.intros [code_pred_intro]
     1.9  
    1.10  code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
    1.11 -unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases)
    1.12 +by (auto elim: A.hd_predicate_in_locale.cases)
    1.13      
    1.14  interpretation A partial_hd .
    1.15  thm hd_predicate_in_locale.intros