Commit ac1ef3c2 authored by MARCHE Claude's avatar MARCHE Claude

Support for Isabelle2013-2

parent f1b24d22
......@@ -134,8 +134,6 @@ orphaned-proofs.prf
/lib/pvs/*/*.summary
pvsbin/
# Isabelle
/lib/isabelle/*/*.xml
# /src/driver/
/src/driver/driver_lexer.ml
......@@ -190,10 +188,6 @@ pvsbin/
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
/examples/*/*.xml
/examples/*/*/*.xml
/examples/*/*/*/*.xml
!why3session.xml
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
......
......@@ -550,15 +550,15 @@ else
ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEVERSION in
2013-1)
2013-2)
enable_isabelle_support=yes
AC_MSG_RESULT($ISABELLEVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle2013-1; Isabelle discarded)
reason_isabelle_support=" (need version 2013-1)"
AC_MSG_WARN(You need Isabelle2013-2; Isabelle discarded)
reason_isabelle_support=" (need version 2013-2)"
;;
esac
fi
......
<theory name="Child_is_son_or_daughter"><realized><require name="why3.BuiltIn"/></realized><typedecl name="person"><params/></typedecl><datatypes><datatype name="gender"><params/><constrs><constr name="Male"/><constr name="Female"/></constrs></datatype></datatypes><param name="gender1"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></param><param name="father"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><param name="mother"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><axiom name="Father_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></concls></axiom><axiom name="Mother_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></concls></axiom><definition><app><const name="HOL.eq"/><app><var name="parent"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="son"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="s"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="daughter"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="d"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="d"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="d"><type name="person" local="true"/></var></app></app></app></definition><lemma name="Child_is_son_or_daughter"><prems/><concls><app><const name="HOL.eq"/><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="son" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="c"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="daughter" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="c"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="Sibling_is_brother_or_sister"><realized><require name="why3.BuiltIn"/></realized><typedecl name="person"><params/></typedecl><datatypes><datatype name="gender"><params/><constrs><constr name="Male"/><constr name="Female"/></constrs></datatype></datatypes><param name="gender1"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></param><param name="father"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><param name="mother"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><axiom name="Father_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></concls></axiom><axiom name="Mother_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></concls></axiom><definition><app><const name="HOL.eq"/><app><var name="parent"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="son"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="s"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="daughter"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="d"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="d"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="d"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="sibling"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="brother"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="b"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="b"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="b"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="sister"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></app></app></definition><lemma name="Sibling_is_brother_or_sister"><prems/><concls><app><const name="HOL.eq"/><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="brother" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="sister" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="Sibling_sym"><realized><require name="why3.BuiltIn"/></realized><typedecl name="person"><params/></typedecl><datatypes><datatype name="gender"><params/><constrs><constr name="Male"/><constr name="Female"/></constrs></datatype></datatypes><param name="gender1"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></param><param name="father"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><param name="mother"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></param><axiom name="Father_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Male" local="true"><type name="gender" local="true"/></const></app></concls></axiom><axiom name="Mother_gender"><prems/><concls><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p"><type name="person" local="true"/></var></app></app><const name="Female" local="true"><type name="gender" local="true"/></const></app></concls></axiom><definition><app><const name="HOL.eq"/><app><var name="parent"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p"><type name="person" local="true"/></var><var name="c"><type name="person" local="true"/></var></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><var name="p"><type name="person" local="true"/></var><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="c"><type name="person" local="true"/></var></app></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="son"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="s"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="s"><type name="person" local="true"/></var></app><const name="Male" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="s"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="daughter"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="d"><type name="person" local="true"/></var><var name="p"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.eq"/><app><const name="gender1" local="true"><fun><type name="person" local="true"/><type name="gender" local="true"/></fun></const><var name="d"><type name="person" local="true"/></var></app><const name="Female" local="true"><type name="gender" local="true"/></const></app><app><const name="parent" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p"><type name="person" local="true"/></var><var name="d"><type name="person" local="true"/></var></app></app></app></definition><definition><app><const name="HOL.eq"/><app><var name="sibling"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></var><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app><app><const name="HOL.conj"/><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.disj"/><app><const name="HOL.eq"/><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="father" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app><app><const name="HOL.eq"/><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p1"><type name="person" local="true"/></var></app><app><const name="mother" local="true"><fun><type name="person" local="true"/><type name="person" local="true"/></fun></const><var name="p2"><type name="person" local="true"/></var></app></app></app></app></app></definition><lemma name="Sibling_sym"><prems><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p1"><type name="person" local="true"/></var><var name="p2"><type name="person" local="true"/></var></app></prems><concls><app><const name="sibling" local="true"><pred><type name="person" local="true"/><type name="person" local="true"/></pred></const><var name="p2"><type name="person" local="true"/></var><var name="p1"><type name="person" local="true"/></var></app></concls></lemma></theory>
\ No newline at end of file
......@@ -36,7 +36,7 @@
<prover
id="8"
name="Isabelle"
version="2013-1"/>
version="2013-2"/>
<prover
id="9"
name="Metis"
......@@ -97,7 +97,7 @@
loclnum="23" loccnumb="7" loccnume="31"
sum="ab198428cded6c66a633de3a5773db5a"
proved="true"
expanded="true"
expanded="false"
shape="adaughterV0V1OasonV0V1qachildV0V1F">
<proof
prover="0"
......@@ -171,7 +171,7 @@
edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"
obsolete="false"
archived="false">
<result status="valid" time="4.77"/>
<result status="valid" time="4.64"/>
</proof>
<proof
prover="9"
......@@ -269,7 +269,7 @@
loclnum="29" loccnumb="7" loccnume="18"
sum="ec0d771fae4cc09506d4a3d021e5dee3"
proved="true"
expanded="true"
expanded="false"
shape="asiblingV1V0IasiblingV0V1F">
<proof
prover="0"
......@@ -334,7 +334,7 @@
edited="genealogy_Genealogy_Sibling_sym_1.xml"
obsolete="false"
archived="false">
<result status="valid" time="4.59"/>
<result status="valid" time="4.58"/>
</proof>
<proof
prover="9"
......@@ -423,7 +423,7 @@
loclnum="34" loccnumb="7" loccnume="35"
sum="de35aeb601cea1cb97be38ceb530a69d"
proved="true"
expanded="true"
expanded="false"
shape="asisterV0V1OabrotherV0V1qasiblingV0V1F">
<proof
prover="0"
......@@ -577,7 +577,7 @@
loclnum="45" loccnumb="7" loccnume="48"
sum="312882150a494c394c83a6719dfc8ffa"
proved="true"
expanded="true"
expanded="false"
shape="agrandmotherV0V1OagrandfatherV0V1qagrandparentV0V1F">
<proof
prover="0"
......
......@@ -443,7 +443,7 @@ name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([^:]+\\)"
version_ok = "2013-1"
version_ok = "2013-2"
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
driver = "drivers/isabelle.drv"
......
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