Re: [isabelle] I want to print axiom info (sledgeH error at end)



On 17.07.2012 09:00, Gottfried Barrow wrote:
--"INFO
BEGIN=================================================================="
--{*notation Trueprop("Tr") notation "prop"("Pr")*}
declare[[show_brackets=true]] declare[[show_sorts=false]]
declare[[names_long=false]] declare[[show_types=true]]
declare[[names_unique=true]] declare[[show_consts=true]]
--"INFO
END--------------------------------------------------------------------"

When you are using jEdit, then I suggest using Ctrl+Hover to get the full names and types of constants, without making the term hardly readable due to all the annotations.





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