--- a/src/HOL/Quickcheck_Exhaustive.thy Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Aug 13 16:25:47 2013 +0200
@@ -447,11 +447,11 @@
begin
definition
- "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
+ "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
where
- "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
+ "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
instance ..
@@ -461,8 +461,8 @@
begin
definition
- "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1)
- orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
+ "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1)
+ orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
where
@@ -476,9 +476,9 @@
begin
definition
- "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1)
- orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2)
- orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3))"
+ "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1)
+ orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2)
+ orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
where
@@ -492,10 +492,10 @@
begin
definition
- "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>1)
- orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>2)
- orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>3)
- orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>4))"
+ "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1)
+ orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2)
+ orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3)
+ orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4))"
definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
where