equal
deleted
inserted
replaced
115 |
115 |
116 |
116 |
117 (* use"ME/solve.sml"; |
117 (* use"ME/solve.sml"; |
118 use"solve.sml"; |
118 use"solve.sml"; |
119 |
119 |
120 val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g"; |
120 val ttt = (Thm.term_of o the o (parse thy))"Substitute [(bdv,x)] g"; |
121 val ttt = (term_of o the o (parse thy))"Rewrite thmid True g"; |
121 val ttt = (Thm.term_of o the o (parse thy))"Rewrite thmid True g"; |
122 |
122 |
123 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f' |
123 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f' |
124 *) |
124 *) |
125 |
125 |
126 |
126 |