]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/closed.xml
basic_rg: reduction was not tail recursive by mistake
[helm.git] / helm / software / matita / closed.xml
1 <?xml version="1.0"?>
2 <b:box xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:b="http://helm.cs.unibo.it/2003/BoxML">
3   <b:h>
4     <b:space width="2em"/>
5     <b:v>
6       <b:space height="2ex"/>
7       <b:v>
8         <b:decor style="box">
9           <b:space width="1ex" height="1ex"/>
10         </b:decor>
11         <b:space height="1ex"/>
12         <b:text>This goal has already been closed.</b:text>
13         <b:text>Use the "skip" command to throw it away.</b:text>
14       </b:v>
15     </b:v>
16   </b:h>
17 </b:box>