| Fri, 08 Apr 2016 20:15:20 +0200 | wenzelm | eliminated unused simproc identifier; | file | diff | annotate |
| Wed, 09 Sep 2015 20:57:21 +0200 | wenzelm | simplified simproc programming interfaces; | file | diff | annotate |
| Sat, 08 Aug 2015 10:51:33 +0200 | haftmann | direct bootstrap of integer division from natural division | file | diff | annotate |
| Sun, 05 Jul 2015 15:02:30 +0200 | wenzelm | simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored); | file | diff | annotate |
| Fri, 24 Oct 2014 15:07:51 +0200 | hoelzl | use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating | file | diff | annotate |
| Thu, 28 Aug 2014 00:40:38 +0200 | blanchet | renamed new SMT module from 'SMT2' to 'SMT' | file | diff | annotate | base |