Hi all,
Albert Steckermeier (steckerm) has just been added to the Isabelle group. He's
a B.Sc. student who is working on an integration of the equality prover
Waldmeister with Sledgehammer. Like all my students, he will get the proper
repository training.
Jasmin
__
I had hoped to have the change I was making to hypothesis-substitution
ready for the coming release.
I've got it working for all of HOL and the library, and begun looking at
the AFP and at the l4.verified proofs. The HOL+library changes were easy
enough, but the l4.verified changes are somewha
