Aesop upddate

Stream: lean4

[Jannis Limperg]

Source code is here: https://github.com/seL4/isabelle/blob/master/src/Provers/clasimp.ML

I'm unsure about too many parts of the notation to really understand what's going on. But maybe I should do some more forensic work.

Btw @Jad Ghalayini sorry about hijacking your thread, it's gone quite far from your original question.

[Patrick Massot]

No more hijacking :wink:

[Patrick Massot]

I think it would really make sense for you to invest time into reading that source code.

[Sebastian Ullrich]

@Joachim Breitner May I summon you regarding your experience with Isabelle & Coq automation, and what directions we should explore with Lean 4? And did you ever get into Isabelle metaprogramming apart from that While language parser for the lab course? :)