Commit 5cc9bf38 authored by Clément Fumex's avatar Clément Fumex
Browse files

correct typo in a new axiom in the bv theory

parent 52897571
......@@ -191,7 +191,7 @@ theory BV_Gen
forall b:t,n s:int. 0 <= n < s ->
nth (lsl b s) n = False
lemma lsl_zero: forall x. lsr x 0 = x
lemma lsl_zero: forall x. lsl x 0 = x
use import int.EuclideanDivision
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment