author | blanchet |
Thu, 01 Nov 2018 14:36:19 +0100 | |
changeset 69220 | c6b15fc78f78 |
parent 69219 | d4cec24a1d87 |
child 69221 | 21ee588bac7d |
--- a/src/HOL/ex/veriT_Preprocessing.thy Thu Nov 01 12:23:54 2018 +0100 +++ b/src/HOL/ex/veriT_Preprocessing.thy Thu Nov 01 14:36:19 2018 +0100 @@ -475,7 +475,7 @@ [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]), N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])])); -reconstruct_proof @{context} proof18 +reconstruct_proof @{context} proof25 \<close> end