Eliminate trivial quantifications in goals

4d2f0191 · Stefan Berghofer · MARCHE Claude · d2e6abc4 · 4d2f0191
Commit 4d2f0191 authored Mar 31, 2015 by Stefan Berghofer Committed by MARCHE Claude Apr 08, 2015
--- a/drivers/isabelle.drv
+++ b/drivers/isabelle.drv
@@ -8,3 +8,5 @@ transformation "inline_trivial"
 transformation "eliminate_builtin"

 import "isabelle-common.gen"
+
+transformation "simplify_trivial_quantification_in_goal"