src/HOL/IMPP/README.html
changeset 51403 2ff3a5589b05
parent 51402 b05cd411d3d3
child 51404 90a598019aeb
equal deleted inserted replaced
51402:b05cd411d3d3 51403:2ff3a5589b05
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
       
     2 
       
     3 <!-- $Id$ -->
       
     4 
       
     5 <HTML>
       
     6 
       
     7 <HEAD>
       
     8   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
       
     9   <TITLE>HOL/IMPP/README</TITLE>
       
    10 </HEAD>
       
    11 
       
    12 <BODY>
       
    13 
       
    14 <H2>IMPP--An imperative language with procedures</H2>
       
    15 
       
    16 This is an extension of <A HREF="../IMP/">IMP</A> with local variables
       
    17 and mutually recursive procedures. For documentation see
       
    18 <A HREF="http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html">
       
    19 Hoare Logic for Mutual Recursion and Local Variables</A>.
       
    20 
       
    21 </BODY></HTML>