src/HOL/ex/Predicate_Compile_ex.thy

 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
 (*quickcheck[generator = pred_compile, size=5, iterations=1]*)
 oops
 
-
 section {* Lambda *}
+
 datatype type =
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 
 datatype dB =