Revision 2998c271bc3a30c4c351c4d39943cf720390cad4 authored by Pierre-Yves Strub on 01 December 2015, 17:10:55 UTC, committed by Pierre-Yves Strub on 01 December 2015, 17:29:46 UTC
Add a new hint mechanism for auto-applying lemmas. Lemmas are added to the auto base with: `hint exact : L1 ... Ln.` `trivial` (and all relatives) now tries to close any goal it is presented by applying one of the lemmas of the database --- closing any generated subgoal recursively. The lemmas in the hint database are not used when `trivial` tries to close the subgoals. Lemmas are applied using a rigid unification and with the view mechanism disabled. The current implementation is linear in the size of the database. A pre-selection mechanism may be necessary in case the hint database grows too much.
1 parent 7cc81de
Computing file changes ...
