ee (Feb 15 2024 at 16:18): ee (Feb 15 2024 at 16:18):I'm trying to use the wf_induct from Wellfounded.thy, yet I'm a bit confused about the syntactic parts, so I'm wondering if anyone knows of another proof or theorem that uses it I could chedck out? I tried searching for it in the AFP but didn't get many results.
TIA
Fabian Huch (Feb 15 2024 at 16:22):Have a look at the findfacts search for things using wf_induct
Last updated: Dec 21 2024 at 16:20 UTC