src/HOL/Quickcheck_Exhaustive.thy
changeset 53015 a1119cf551e8
parent 52435 6646bb548c6b
child 58152 6fe60a9a5bad
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -447,11 +447,11 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
     1.8 +  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
     1.9  
    1.10  definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
    1.11  where
    1.12 -  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
    1.13 +  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
    1.14  
    1.15  instance ..
    1.16  
    1.17 @@ -461,8 +461,8 @@
    1.18  begin
    1.19  
    1.20  definition
    1.21 -  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1)
    1.22 -    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
    1.23 +  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1)
    1.24 +    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
    1.25  
    1.26  definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
    1.27  where
    1.28 @@ -476,9 +476,9 @@
    1.29  begin
    1.30  
    1.31  definition
    1.32 -  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1)
    1.33 -    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2)
    1.34 -    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3))"
    1.35 +  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1)
    1.36 +    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2)
    1.37 +    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
    1.38  
    1.39  definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
    1.40  where
    1.41 @@ -492,10 +492,10 @@
    1.42  begin
    1.43  
    1.44  definition
    1.45 -  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>1)
    1.46 -    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>2)
    1.47 -    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>3)
    1.48 -    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>4))"
    1.49 +  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1)
    1.50 +    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2)
    1.51 +    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3)
    1.52 +    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4))"
    1.53  
    1.54  definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
    1.55  where