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