Commit dc8d92b8 authored by MARCHE Claude's avatar MARCHE Claude

example for issue #269, can't reproduce

parent 1545723d
use int.Int
constant a : int
constant b : int
axiom H : a = b
goal G : if a > 0 then true else false
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<file>
<path name=".."/>
<path name="269_replace_under_if.mlw"/>
<theory name="Top">
<goal name="G">
<transf name="replace" arg1="a" arg2="b">
<goal name="G.0">
</goal>
<goal name="G.1" expl="equality hypothesis">
</goal>
</transf>
<transf name="rewrite" arg1="H">
<goal name="G.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment