changeset 71959 | ee2c7f0dd1be |
parent 71918 | 4e0a58818edc |
--- a/src/HOL/Proofs/Lambda/NormalForm.thy Thu Jun 18 09:07:54 2020 +0000 +++ b/src/HOL/Proofs/Lambda/NormalForm.thy Fri Jun 19 09:46:47 2020 +0000 @@ -92,7 +92,7 @@ apply (induct m) apply (case_tac n) apply (case_tac [3] n) - apply (simp del: simp_thms subst_all subst_all', iprover?)+ + apply (simp del: simp_thms subst_all, iprover?)+ done lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"