src/FOL/ex/Nat2.ML
changeset 1959 58f8379eca73
parent 1662 a6b55b9d2f22
child 2469 b50b8c0eec01
equal deleted inserted replaced
1958:6f20ecbd87cb 1959:58f8379eca73
   132 goal Nat2.thy "i<=j --> j<=k --> i<=k";
   132 goal Nat2.thy "i<=j --> j<=k --> i<=k";
   133 by (IND_TAC nat_ind (K all_tac) "i" 1);
   133 by (IND_TAC nat_ind (K all_tac) "i" 1);
   134 by (simp_tac nat_ss 1);
   134 by (simp_tac nat_ss 1);
   135 by (resolve_tac [impI RS allI] 1);
   135 by (resolve_tac [impI RS allI] 1);
   136 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
   136 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
       
   137 by (resolve_tac [impI] 1);
   137 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
   138 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
   138 by (fast_tac FOL_cs 1);
   139 by (fast_tac FOL_cs 1);
   139 qed "le_trans";
   140 qed "le_trans";
   140 
   141 
   141 goal Nat2.thy "i < j --> j <=k --> i < k";
   142 goal Nat2.thy "i < j --> j <=k --> i < k";