src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 44890 22f665a2e91c
parent 42463 f270e3e18be5
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4      from alt_nil nil show thesis by auto
     1.5    next
     1.6      case cons
     1.7 -    from alt_cons cons show thesis by fastsimp
     1.8 +    from alt_cons cons show thesis by fastforce
     1.9    qed
    1.10  qed
    1.11  
    1.12 @@ -469,7 +469,7 @@
    1.13    next
    1.14      fix xs ys zs x
    1.15      assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
    1.16 -    from this append2(2) show thesis by fastsimp
    1.17 +    from this append2(2) show thesis by fastforce
    1.18    qed
    1.19  qed
    1.20  
    1.21 @@ -913,7 +913,7 @@
    1.22    assume "has_length xs i" "has_length ys i" "r (x, y)"
    1.23    from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
    1.24      unfolding lexn_conv Collect_def mem_def
    1.25 -    by fastsimp
    1.26 +    by fastforce
    1.27  next
    1.28    assume "lexn r i (xs, ys)"
    1.29    thm lexn_conv
    1.30 @@ -935,8 +935,8 @@
    1.31      apply (auto simp add: has_length)
    1.32      apply (case_tac xys)
    1.33      apply auto
    1.34 -    apply fastsimp
    1.35 -    apply fastsimp done
    1.36 +    apply fastforce
    1.37 +    apply fastforce done
    1.38  qed
    1.39  
    1.40  values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"