Hi, I have a situation where I don't know what the best solution is.
I have a goal of the form x ==> y, and after an initial rewrite on x and after REPEAT STRIP_TAC, I have a list of subgoals. Here's the problem. 1) According to different situations, the length of the list of subgoals varies; 2) For each subgoal, I need use a different concrete term to instantiate a variable. The term is prepared for each subgoal. I don't know if I can implement this by programming in tactics or on the goal stack. I appreciate any suggestions. Thanks Lu ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
