src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 60565 b7ee41f72add
parent 58310 91ea607a34d8
child 62121 c8a93680b80d
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Jun 24 00:30:03 2015 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Jun 24 21:26:03 2015 +0200
     1.3 @@ -241,10 +241,10 @@
     1.4    from appending.prems show thesis
     1.5    proof(cases)
     1.6      case nil
     1.7 -    from alt_nil nil show thesis by auto
     1.8 +    from appending.alt_nil nil show thesis by auto
     1.9    next
    1.10      case cons
    1.11 -    from alt_cons cons show thesis by fastforce
    1.12 +    from appending.alt_cons cons show thesis by fastforce
    1.13    qed
    1.14  qed
    1.15  
    1.16 @@ -270,17 +270,17 @@
    1.17    from ya_even.prems show thesis
    1.18    proof (cases)
    1.19      case even_zero
    1.20 -    from even_zero even_0 show thesis by simp
    1.21 +    from even_zero ya_even.even_0 show thesis by simp
    1.22    next
    1.23      case even_plus1
    1.24 -    from even_plus1 even_Suc show thesis by simp
    1.25 +    from even_plus1 ya_even.even_Suc show thesis by simp
    1.26    qed
    1.27  next
    1.28    case ya_odd
    1.29    from ya_odd.prems show thesis
    1.30    proof (cases)
    1.31      case odd_plus1
    1.32 -    from odd_plus1 odd_Suc show thesis by simp
    1.33 +    from odd_plus1 ya_odd.odd_Suc show thesis by simp
    1.34    qed
    1.35  qed
    1.36