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
smime.p7s
Description: S/MIME Kryptografische Unterschrift
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
