Removed comments.
authornipkow
Thu, 06 Aug 1998 12:44:07 +0200
changeset 5269 3155ccd9a506
parent 5268 59ef39008514
child 5270 70c599bff977
Removed comments.
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;