equal
deleted
inserted
replaced
148 val t'' = subst_atomic subst t'; |
148 val t'' = subst_atomic subst t'; |
149 term2str t''; |
149 term2str t''; |
150 (********"0 = 3 * 0"*) |
150 (********"0 = 3 * 0"*) |
151 |
151 |
152 val thm = assoc_thm' thy ("sym",""); |
152 val thm = assoc_thm' thy ("sym",""); |
153 (*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! |
153 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! |
154 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; |
154 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; |
155 *) |
155 *) |
156 |
156 |
157 (* use"../smltest/IsacKnowledge/algein.sml"; |
157 (* use"../smltest/IsacKnowledge/algein.sml"; |
158 *) |
158 *) |