Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Refinement Framework

Email Gateway (Jun 29 2022 at 06:56):

From: Valentin Springsklee <uidpn@student.kit.edu>
Hello,

I found the solution already. It turned out, that it is the same as
shoing termination of any function. I was just confused about the syntax
when appliyng the WHILET_rule.

I am fairly new to Isabelle and I should probably have posted this
kind of question on the Zulip chat. Sorry for theinconvenience

Kind regards,

Valentin Springsklee

Last updated: Jan 04 2025 at 20:18 UTC