diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Coind/Values.thy --- a/src/ZF/Coind/Values.thy Tue Sep 27 17:54:20 2022 +0100 +++ b/src/ZF/Coind/Values.thy Tue Sep 27 18:02:34 2022 +0100 @@ -67,7 +67,7 @@ lemma v_constNE [simp]: "c \ Const \ v_const(c) \ 0" -apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs) + unfolding QPair_def QInl_def QInr_def Val_ValEnv.con_defs apply (drule constNEE, auto) done