Hi, Tobias Thanks for the reply. My main motivation here is to try to write something that more closely resembles how humans think. I understand this is very far from being able to be included in the main repository. This is just to explore different approaches.
In particular I would be interested in test cases that are simple for a human (so we may expect the computer to solve it during proof development), but difficult for a BFS rewriter like this, because they may show some heuristics that humans use, that perhaps can be incorporated into an automated prover. Best, Bohua _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
