more
authorblanchet
Thu Nov 01 14:36:19 2018 +0100 (6 months ago)
changeset 69220c6b15fc78f78
parent 69219 d4cec24a1d87
child 69221 21ee588bac7d
more
src/HOL/ex/veriT_Preprocessing.thy
     1.1 --- a/src/HOL/ex/veriT_Preprocessing.thy	Thu Nov 01 12:23:54 2018 +0100
     1.2 +++ b/src/HOL/ex/veriT_Preprocessing.thy	Thu Nov 01 14:36:19 2018 +0100
     1.3 @@ -475,7 +475,7 @@
     1.4       [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]),
     1.5        N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])]));
     1.6  
     1.7 -reconstruct_proof @{context} proof18
     1.8 +reconstruct_proof @{context} proof25
     1.9  \<close>
    1.10  
    1.11  end