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