diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Coind/Values.thy --- a/src/ZF/Coind/Values.thy Tue Sep 27 17:46:52 2022 +0100 +++ b/src/ZF/Coind/Values.thy Tue Sep 27 17:54:20 2022 +0100 @@ -101,7 +101,7 @@ done lemma ve_empI: "ve_emp \ ValEnv" -apply (unfold ve_emp_def) + unfolding ve_emp_def apply (rule Val_ValEnv.intros) apply (rule pmap_empI) done