Skip to content
Success

Changes

Summary

  1. replaced minimality argument a la Baader & Nipkow by an induction
Changeset 7345:e04aeed2b06f by blanchet:
replaced minimality argument a la Baader & Nipkow by an induction
The file was modified thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy (diff)