doc-src/Tutorial/Misc/arith3.ML
author paulson
Thu, 16 Nov 2000 10:47:11 +0100
changeset 10475 77fafa07fc8f
parent 6577 a2b5c84d590a
permissions -rw-r--r--
ground terms section: new intro

Goal "~ m < n & m < n+1 ==> m = n";