doc-src/Tutorial/Misc/arith1.ML
changeset 6577 a2b5c84d590a
equal deleted inserted replaced
6576:7e0b35bed503 6577:a2b5c84d590a
       
     1 Goal "[| ~ m < n; m < n+1 |] ==> m = n";