src/ZF/ord.ML
changeset 37 cebe01deba80
parent 30 d49df4181f0d
child 186 320f6bdb593a
equal deleted inserted replaced
36:70c6014c9b6f 37:cebe01deba80
   378 goal Ord.thy "!!i. Ord(i) ==> 0 le i";
   378 goal Ord.thy "!!i. Ord(i) ==> 0 le i";
   379 by (etac (not_lt_iff_le RS iffD1) 1);
   379 by (etac (not_lt_iff_le RS iffD1) 1);
   380 by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));
   380 by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));
   381 val Ord_0_le = result();
   381 val Ord_0_le = result();
   382 
   382 
   383 goal Ord.thy "!!i. [| Ord(i);  ~ i=0 |] ==> 0<i";
   383 goal Ord.thy "!!i. [| Ord(i);  i~=0 |] ==> 0<i";
   384 by (etac (not_le_iff_lt RS iffD1) 1);
   384 by (etac (not_le_iff_lt RS iffD1) 1);
   385 by (rtac Ord_0 1);
   385 by (rtac Ord_0 1);
   386 by (fast_tac lt_cs 1);
   386 by (fast_tac lt_cs 1);
   387 val Ord_0_lt = result();
   387 val Ord_0_lt = result();
   388 
   388