*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] parse translations and lexical matters*From*: Matthias Schmalz <Matthias.Schmalz at inf.ethz.ch>*Date*: Fri, 14 Jan 2011 21:37:21 +0100*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Hi, I have two questions: 1. Consider the following contrieved parse translation translating "foo x. t" to "(\<forall> x. t) \<and> (\<forall> x. t)": syntax "_foo" :: "idt => 'a => bool" ("foo _. _") parse_translation {* let val forall_tr = snd (mk_binder_tr ("\<forall> ", @{const_syntax All})) fun foo_tr [idt, t] = let val all = forall_tr [idt, t] in @{const "op &"} $ all $ all end in [(@{syntax_const "_foo"}, foo_tr)] end *} When I execute term "foo x. True" (with show_types activated) I get "(\<forall> x::'a. True) \<and> (\<forall> x::'b. True)". (The two occurrences of x have different types.) Is it possible to change the parse translation so that term "foo x. True" yields "(\<forall> x::'a. True) \<and> (\<forall> x::'a. True)". (The two occurrences of x have the same type.) 2. I am translating terms from some other logic (i.e., Event-B) to Isabelle/HOL. For that I need to know which identifiers (i.e., tokens of the category ident, p. 28 of the reference manual) I can use as variable names. I do already know that I cannot use the tokens listed in the section "lexicon" of the output of "print_syntax". I have also discovered that tokens with a trailing underscore and the token "dummy_pattern" cannot be used as variable names. I wonder whether there are more such tokens and how I can get an at least approximate list of them. Thanks for any help, Matthias -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFNMLQBczhznXSdWggRAp7UAJ9M74KKj3Lid6OTneUENvnwms2TXACgprT9 CedcBF7gH5x5ArSZC5M04sg= =UBu+ -----END PGP SIGNATURE-----

**Follow-Ups**:**Re: [isabelle] parse translations***From:*Makarius

**Re: [isabelle] lexical matters***From:*Makarius

- Previous by Date: [isabelle] 2nd CfP: JAL Special Issue on Automated Specification and Verification of Web Systems
- Next by Date: [isabelle] When to expect working duals with locales?
- Previous by Thread: [isabelle] 2nd CfP: JAL Special Issue on Automated Specification and Verification of Web Systems
- Next by Thread: Re: [isabelle] parse translations
- Cl-isabelle-users January 2011 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