# [isabelle] I want to print axiomatization info

Hi,
I have a function:
axiomatization--"Set membership predicate."

` in\<^isub>\<sigma>::"\<sigma>\<^isub>t \<Rightarrow>
``\<sigma>\<^isub>t \<Rightarrow> \<sigma>\<^isub>t\<^isub>b" ("_
``\<in>\<^isub>\<sigma> _" 55)
`
I then state multiple axioms about it, one of them being:
axiomatization--"Axiom schema of comprehension: schema set." where

` \<Sigma>\<^isub>s\<^isub>c\<^isub>A: "\<forall>u. \<forall>P.
``\<exists>a. \<forall>x.(x \<in>\<^isub>\<sigma> a \<longleftrightarrow>
``(x \<in>\<^isub>\<sigma> u \<and> P x))"
`

`I want to look at how Isabelle decided to type variables in my
``axiomatization, but I can't find any print or find commands that will do
``that for me. I also want to see if explicit parentheses will be added as
``I expect, and see if there are any operator priority surprises.
`
Is there such a command that will do this for me?
The above is the basic question. Here's what led me to want to know this:
1) I used "\<in>" as notation for my set membership.

`2) I got lots of warnings like: "Ambiguous input produces 4 parse
``trees... Fortunately, only one parse tree is type correct..."
``3) I change my notation to " \<in>\<^isub>\<sigma>", and it gets rid of
``some of the warnings.
``4) For the axiom above, I still get "ambiguous" warnings, with some of
``the variables explicitly typed.
``5) So, I explicitly type every variable in the formula, and I still get
``"ambiguous" warnings.
``6) So, I remove all the typing, and it seems to work. Explicit or
``non-explicit typing doesn't affect the warnings.
``7) I then conclude that Isabelle gets all of the typing information in
``the formula from my one uniquely named function, "in\<^isub>\<sigma>".
``Consequently, I ask myself, "Is that too good to be true?"
`

`Okay, if I knew how to prove anything, maybe I would know how to get the
``information I want. However, even if I was an expert, I would want to be
``able to get immediate feedback to check my typing, see if I'm correctly
``using parentheses, and see if I understand correctly the priority of the
``operators.
`

`I attach a screen shot of my code. I don't think attaching images and
``PDFs is the best way to give people code information. On the other hand,
``the above low-level Isar shows that nice looking things in jEdit cease
``to be good for reading in a text file. Also, "\<^isub>" doesn't result
``in subscripted, unicode characters when copying and pasting.
`

`jEdit Stuff: I edited the etc/symbols file and jEdit gave me an
``exception error when loading. Afterwards, jEdit wouldn't translate
``commands like "\<in>" in the one file. About an hour later, or two, I
``deleted "jEdit/recent.xml" and it started working again.
`
Regards,
GB

**Attachment:
**`wantToPrintAxiomInfo.png`

*Description:* PNG image

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