Re: [isabelle] thin_tac



On Thu, 27 Nov 2014, Lars Noschinski wrote:

is there a deeper reason why thin_tac allows schematics in the pattern, but no underscores?

thin_tac belongs to the res_inst_tac family, which has the following comment in the ML sources: (* FIXME cleanup this mess!!! *) -- it means that this is highly non-canonical within Isar, and dummy patterns via underscore belong to certain Isar syntax policies that are not observed here.

After so many years of these remaining oddities in the sources, there is actually a perspective to overcome it all, and have proof methods with a goal focus that fit into Isar conceptually -- as part of the Eisbach work.


	Makarius

----------------------------------------------------------------------------
                  http://stop-ttip.org  980,792 people so far
----------------------------------------------------------------------------




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