Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop


Am Montag, den 23.02.2015, 16:51 +0100 schrieb Christian Sternagel:
> quick (unrelated) question ;)
> How is your "open inductive" related to the AFP entry "Open Induction"?

good question. I would assume not at all, as it is not listed in [1] :-)

In "open inductive predicate", you have to associate the words to the
right, i.e. "open (inductive predicates)". The idea is that you can
modularize your inducrive predicates and inductive proofs, something
that I often want to do when working with programming language
semantics. There is not much deep theory, but rather itâs making the
obvious (namely that the cases of inductive proofs are independent)
exploitable. See [1] for more details (motivation, examples, user

In your entry, if I am not mistaken, "open" refers to topology.



Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.