Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP/devel entry: Open Induction

view this post on Zulip Email Gateway (Aug 19 2022 at 09:30):

From: Tobias Nipkow <nipkow@in.tum.de>
Mizuhito Ogawa and Christian Sternagel

A proof of the open induction schema based on J.-C. Raoult, Proving open
properties by induction, Information Processing Letters 29, 1988, pp.19-23.

http://afp.sourceforge.net/devel-entries/Open_Induction.shtml
Development version only

Enjoy!

Last updated: Apr 26 2024 at 12:28 UTC