*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Sort hypotheses in proof*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 20 Oct 2015 17:18:29 +0200*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear list, today I noticed a funny suffix in my goal state: using this: wellformed 0 t' rs â t â* t' [evaluate] Peter informed me that "[evaluate]" is a (pending?) sort hypothesis. However, I've seen some inconsistent behaviour in which cases exactly those are printed. Consider the following minimal theory (see also attachment): typedecl rules consts rules :: "rules â bool" class evaluate = fixes eval :: "'a â bool" assumes eval_valid: "rules rs â eval a" definition scoped_eval_fun where "scoped_eval_fun rs f â (âx. eval x â eval (f x))" lemma "rules rs â scoped_eval_fun rs a" proof - fix rs assume "rules rs" thm this thm ârules rsâ oops In the proof, I expected that either both "thm" statements print the sort hypothesis, or both don't. In reality, if I reference a fact by name, it won't show up; only, if I reference it by a literal. This confuses me tremendously, especially given that the fact "rules rs" doesn't stem from the class. Cheers Lars

**Attachment:
Hyps.thy**

**Follow-Ups**:**Re: [isabelle] Sort hypotheses in proof***From:*Makarius

- Previous by Date: Re: [isabelle] Redefine or hook into the outer-syntax keywords
- Next by Date: [isabelle] Sum of first n integers
- Previous by Thread: Re: [isabelle] Redefine or hook into the outer-syntax keywords
- Next by Thread: Re: [isabelle] Sort hypotheses in proof
- Cl-isabelle-users October 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list