@@ -18,6 +18,20 @@
1818 sodipodi:docname="compareToProofAssist.svg">
1919 <defs
2020 id="defs4">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker4251"
25+ refX="0.0"
26+ refY="0.0"
27+ orient="auto"
28+ inkscape:stockid="Arrow1Mend">
29+ <path
30+ transform="scale(0.4) rotate(180) translate(10,0)"
31+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
32+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
33+ id="path4253" />
34+ </marker>
2135 <marker
2236 inkscape:stockid="Arrow1Mend"
2337 orient="auto"
@@ -89,7 +103,7 @@
89103 <dc:format>image/svg+xml</dc:format>
90104 <dc:type
91105 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
92− <dc:title></dc:title>
106+ <dc:title />
93107 </cc:Work>
94108 </rdf:RDF>
95109 </metadata>
@@ -167,56 +181,37 @@
167181 style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4436)"
168182 inkscape:export-xdpi="61.120499"
169183 inkscape:export-ydpi="61.120499" />
170− <text
171− sodipodi:linespacing="125%"
172− id="text4998"
173− y="307.36221"
174− x="306"
175− style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
176− xml:space="preserve"
177− inkscape:export-xdpi="61.120499"
178− inkscape:export-ydpi="61.120499"><tspan
179− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
180− y="307.36221"
181− x="306"
182− id="tspan5000"
183− sodipodi:role="line">High level program</tspan><tspan
184− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
185− y="326.11221"
186− x="306"
187− sodipodi:role="line"
188− id="tspan5058">(unification algorithm)</tspan></text>
189184 <text
190185 xml:space="preserve"
191186 style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
192− x="316"
193− y="369.36221"
187+ x="314"
188+ y="326.36221"
194189 id="text5002"
195190 sodipodi:linespacing="125%"
196191 inkscape:export-xdpi="61.120499"
197192 inkscape:export-ydpi="61.120499"><tspan
198193 sodipodi:role="line"
199194 id="tspan5004"
200− x="316"
201− y="369.36221"
202− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">Tactics</tspan></text>
195+ x="314"
196+ y="326.36221"
197+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">Idris source</tspan></text>
203198 <text
204199 sodipodi:linespacing="125%"
205200 id="text5006"
206− y="416.36221"
207− x="315"
201+ y="413.36221"
202+ x="281"
208203 style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
209204 xml:space="preserve"
210205 inkscape:export-xdpi="61.120499"
211206 inkscape:export-ydpi="61.120499"><tspan
212207 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
213− y="416.36221"
214− x="315"
208+ y="413.36221"
209+ x="281"
215210 id="tspan5008"
216211 sodipodi:role="line">fill holes</tspan><tspan
217212 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
218− y="435.11221"
219− x="315"
213+ y="432.11221"
214+ x="281"
220215 sodipodi:role="line"
221216 id="tspan5060">(implicit variables, etc)</tspan></text>
222217 <text
@@ -237,7 +232,7 @@
237232 inkscape:connector-curvature="0"
238233 id="path5014"
239234 d="m 342,330.3622 0,22"
240− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
235+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4251)"
241236 inkscape:export-xdpi="61.120499"
242237 inkscape:export-ydpi="61.120499" />
243238 <path
@@ -247,5 +242,19 @@
247242 inkscape:connector-curvature="0"
248243 inkscape:export-xdpi="61.120499"
249244 inkscape:export-ydpi="61.120499" />
245+ <text
246+ inkscape:export-ydpi="61.120499"
247+ inkscape:export-xdpi="61.120499"
248+ sodipodi:linespacing="125%"
249+ id="text4247"
250+ y="369.36221"
251+ x="317"
252+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
253+ xml:space="preserve"><tspan
254+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
255+ y="369.36221"
256+ x="317"
257+ id="tspan4249"
258+ sodipodi:role="line">Tactics</tspan></text>
250259 </g>
251260</svg>