[isabelle-dev] Mixfix-Syntax not recognized

[René Neumann]

Am 06.08.2013 16:41, schrieb René Neumann:
> Hi,
> 
> I'm currently on revision 8d8cb75ab20a, and mixfix-Syntax seems not
> recognized in all cases (it seems like the syntax is only recognized if
> the type is known, somewhat...).
> 
> Toy-Example (⇧ = \<^sup>) :
> 
> begin
> definition foo :: "'a list ⇒ nat" ("(_⇧ω)") where
> "foo xs = length xs"
> 
> term "foo xs" -- "type nat (as expected)"
> term "xs⇧ω" -- "type 'a"
> term "(xs::'a list)⇧ω" -- "type nat (as expected)"

"xs ⇧ω" (note the space) works.

- René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4782 bytes
Desc: S/MIME Kryptografische Unterschrift
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130806/5a30a15b/attachment.bin>