1structure recordEnumSimpsLib =
2struct
3
4  open simpLib BasicProvers
5
6  val stupid_lemma = Q.prove(���x < 10 ==> x < 11���,
7                             SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) []);
8
9end
10