# HG changeset patch
# User nipkow
# Date 902400247 -7200
# Node ID 3155ccd9a5069956f9bd41a06f17671bf471dc99
# Parent  59ef39008514b01fba4e755f2bf6fc5d2e887b93
Removed comments.

diff -r 59ef39008514 -r 3155ccd9a506 src/HOL/Lambda/InductTermi.ML
--- a/src/HOL/Lambda/InductTermi.ML	Thu Aug 06 12:24:04 1998 +0200
+++ b/src/HOL/Lambda/InductTermi.ML	Thu Aug 06 12:44:07 1998 +0200
@@ -46,13 +46,6 @@
     ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"];
 AddSEs IT_cases;
 
-(* FIXME
-"Arith.trans_less_add1",   "?i < ?j ==> ?i < ?j + ?m"
-"Arith.less_imp_add_less", "?m < ?n ==> ?m < ?n + ?k"
-"Arith.trans_le_add1", "?i <= ?j ==> ?i <= ?j + ?m"
-"Arith.le_imp_add_le", "?m <= ?n ==> ?m <= ?n + ?k"
-*)
-
 Goal "t : termi beta ==> \
 \     !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)";
 be acc_induct 1;