| Mon, 11 Aug 2014 10:43:03 +0200 | traytel | use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed) | file | diff | annotate |
| Wed, 23 Apr 2014 17:57:56 +0200 | kuncar | predicator simplification rules: support also partially specialized types e.g. 'a * nat | file | diff | annotate |
| Thu, 10 Apr 2014 17:48:18 +0200 | kuncar | setup for Transfer and Lifting from BNF; tuned thm names | file | diff | annotate |