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



Hi,

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
guide).

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

Greetings,
Joachim

[1] http://pp.ipd.kit.edu/uploads/publikationen/molitor15masterarbeit.pdf


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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