Re: [isabelle] Schematic vars or universal bound vars in theorem?



On Wed, 18 Jul 2012, Gottfried Barrow wrote:

It's my healthy paranoia kicking in here. I'm using axioms, so I'm trying to use everything I know right now to keep from being inconsistent.

The best way is not to use axioms then. In mathematics you define new things by using old ones, and then prove the desired properties. Sometimes you work with abstract theories, but that corresponds to a locale or class definition in Isabelle/HOL, not axiomatization.


	Makarius





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