# HG changeset patch
# User blanchet
# Date 1541079379 -3600
# Node ID c6b15fc78f7813a82622b2f5d29cb7327d9580e2
# Parent  d4cec24a1d87d97fa18de436ad42ba016e9dec7e
more

diff -r d4cec24a1d87 -r c6b15fc78f78 src/HOL/ex/veriT_Preprocessing.thy
--- 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