# HG changeset patch
# User blanchet
# Date 1541060758 -3600
# Node ID a8c707352ccc36e7c3881d41bbed1a72b13a48f5
# Parent  1a52baa70aed63c44e8ab1d28fbc5cac7cda0ba9
added an example

diff -r 1a52baa70aed -r a8c707352ccc src/HOL/ex/veriT_Preprocessing.thy
--- a/src/HOL/ex/veriT_Preprocessing.thy	Wed Oct 31 15:53:32 2018 +0100
+++ b/src/HOL/ex/veriT_Preprocessing.thy	Thu Nov 01 09:25:58 2018 +0100
@@ -467,4 +467,15 @@
 reconstruct_proof @{context} proof24
 \<close>
 
+ML \<open>
+val proof25 =
+  ((@{term "let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat"},
+    @{term "vr1 + vr2 + vr2 :: nat"}),
+   N (Trans @{term "let vr1a = vr2 in vr1 + vr1a + vr2 :: nat"},
+     [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]),
+      N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])]));
+
+reconstruct_proof @{context} proof18
+\<close>
+
 end