equal
deleted
inserted
replaced
275 | mk(Nat(i)) = ((*writeln"N";*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))) |
275 | mk(Nat(i)) = ((*writeln"N";*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))) |
276 | mk(LessD(j)) = ((*writeln"L";prth*)(hd([mk j] RL !LA_Data.lessD))) |
276 | mk(LessD(j)) = ((*writeln"L";prth*)(hd([mk j] RL !LA_Data.lessD))) |
277 | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD)) |
277 | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD)) |
278 | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD))) |
278 | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD))) |
279 | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD)) |
279 | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD)) |
280 | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp(prth(addthms (mk j1) (mk j2))))) |
280 | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp((*prth*)(addthms (mk j1) (mk j2))))) |
281 | mk(Multiplied(n,j)) = ((*writeln"*";*)multn(n,mk j)) |
281 | mk(Multiplied(n,j)) = ((*writeln"*";*)multn(n,mk j)) |
282 |
282 |
283 in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end |
283 in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end |
284 end; |
284 end; |
285 |
285 |