Mentions légales du service

Skip to content
Snippets Groups Projects
Select Git revision
  • coma_brass
  • new-dune
  • master default protected
  • weekly_full_bench
  • 920-counterexample-parsing-is-wrong-on-floating-point-value
  • coma-while
  • post-release-181
  • alt-ergo-js
  • support_for_bv_overflow_checks
  • btjorge/test
  • bugfix/v1.8 protected
  • stable protected
  • bv-coq9
  • lident_doc
  • 894-extraction-broken-when-cloning-a-module-with-interface
  • test
  • 910-distinct-theories-with-the-same-ident
  • feature/update-colibri2-drv
  • strange-high-failure-with-alt-ergo-2-6-0
  • 908-colibri-driver-with-most-recent-colibri
  • 1.8.1
  • 1.8.0
  • 1.7.2
  • 1.7.1
  • 1.7.0
  • 1.6.0
  • 1.5.1
  • 1.5.0
  • 1.4.1
  • 1.4.0
  • 1.3.3
  • 1.3.2
  • 1.3.1
  • 1.3.0
  • 1.2.1
  • 1.2.0
  • 1.1.1
  • 1.1.0
  • 1.0.0
  • 0.88.3
40 results
Blame Permalink
isabelle2016.drv 325 B 
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)

printer "isabelle"
filename "%f_%t_%g.xml"

transformation "inline_trivial"
transformation "eliminate_builtin"

import "isabelle-common.gen"
import "isabelle-2016.gen"


transformation "simplify_trivial_quantification_in_goal"