src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
 changeset 53374 a14d2a854c02 parent 53072 acc495621d72 child 58249 180f1b3508ed
```     1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 03 00:51:08 2013 +0200
1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 03 01:12:40 2013 +0200
1.3 @@ -54,7 +54,8 @@
1.4    sorted_single [code_pred_intro]
1.5    sorted_many [code_pred_intro]
1.6
1.7 -code_pred sorted proof -
1.8 +code_pred sorted
1.9 +proof -
1.10    assume "sorted xa"
1.11    assume 1: "xa = [] \<Longrightarrow> thesis"
1.12    assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
1.13 @@ -65,9 +66,12 @@
1.14      case (Cons x xs) show ?thesis proof (cases xs)
1.15        case Nil with Cons 2 show ?thesis by simp
1.16      next
1.17 -      case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
1.18 -      moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
1.19 -      ultimately show ?thesis by (rule 3)
1.20 +      case (Cons y zs)
1.21 +      show ?thesis
1.22 +      proof (rule 3)
1.23 +        from Cons `xa = x # xs` show "xa = x # y # zs" by simp
1.24 +        with `sorted xa` show "x \<le> y" and "sorted (y # zs)" by simp_all
1.25 +      qed
1.26      qed
1.27    qed
1.28  qed
```