Hi, Does anyone know of a good way to rewrite a definition wrt. other axioms? For example, given:
a1: "ALL x. f x = g x + h x" a2: "ALL x. g x = m x * n x" I'm trying to get a new axiom: ax1': "ALL x. f x = (m x * n x) + h x", i.e. rewriting a1 using a2. Is there already an existing mechanism that does this? Otherwise, what is the best angle to approach this? Thanks John _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
