added an example
authorblanchet
Thu Nov 01 09:25:58 2018 +0100 (6 months ago)
changeset 69217a8c707352ccc
parent 69216 1a52baa70aed
child 69218 59aefb3b9e95
added an example
src/HOL/ex/veriT_Preprocessing.thy
     1.1 --- a/src/HOL/ex/veriT_Preprocessing.thy	Wed Oct 31 15:53:32 2018 +0100
     1.2 +++ b/src/HOL/ex/veriT_Preprocessing.thy	Thu Nov 01 09:25:58 2018 +0100
     1.3 @@ -467,4 +467,15 @@
     1.4  reconstruct_proof @{context} proof24
     1.5  \<close>
     1.6  
     1.7 +ML \<open>
     1.8 +val proof25 =
     1.9 +  ((@{term "let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat"},
    1.10 +    @{term "vr1 + vr2 + vr2 :: nat"}),
    1.11 +   N (Trans @{term "let vr1a = vr2 in vr1 + vr1a + vr2 :: nat"},
    1.12 +     [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]),
    1.13 +      N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])]));
    1.14 +
    1.15 +reconstruct_proof @{context} proof18
    1.16 +\<close>
    1.17 +
    1.18  end