src/HOL/Library/Product_Lexorder.thy
 changeset 53015 a1119cf551e8 parent 52729 412c9e0381a1 child 54863 82acc20ded73
```     1.1 --- a/src/HOL/Library/Product_Lexorder.thy	Tue Aug 13 14:20:22 2013 +0200
1.2 +++ b/src/HOL/Library/Product_Lexorder.thy	Tue Aug 13 16:25:47 2013 +0200
1.3 @@ -94,23 +94,23 @@
1.4      case (Pair a b)
1.5      show "P (a, b)"
1.6      proof (induct a arbitrary: b rule: less_induct)
1.7 -      case (less a\<^isub>1) note a\<^isub>1 = this
1.8 -      show "P (a\<^isub>1, b)"
1.9 +      case (less a\<^sub>1) note a\<^sub>1 = this
1.10 +      show "P (a\<^sub>1, b)"
1.11        proof (induct b rule: less_induct)
1.12 -        case (less b\<^isub>1) note b\<^isub>1 = this
1.13 -        show "P (a\<^isub>1, b\<^isub>1)"
1.14 +        case (less b\<^sub>1) note b\<^sub>1 = this
1.15 +        show "P (a\<^sub>1, b\<^sub>1)"
1.16          proof (rule P)
1.17 -          fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
1.18 +          fix p assume p: "p < (a\<^sub>1, b\<^sub>1)"
1.19            show "P p"
1.20 -          proof (cases "fst p < a\<^isub>1")
1.21 +          proof (cases "fst p < a\<^sub>1")
1.22              case True
1.23 -            then have "P (fst p, snd p)" by (rule a\<^isub>1)
1.24 +            then have "P (fst p, snd p)" by (rule a\<^sub>1)
1.25              then show ?thesis by simp
1.26            next
1.27              case False
1.28 -            with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
1.29 +            with p have 1: "a\<^sub>1 = fst p" and 2: "snd p < b\<^sub>1"
1.30                by (simp_all add: less_prod_def')
1.31 -            from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
1.32 +            from 2 have "P (a\<^sub>1, snd p)" by (rule b\<^sub>1)
1.33              with 1 show ?thesis by simp
1.34            qed
1.35          qed
```