src/LCF/ROOT
changeset 48475 02dd825f5a4e
child 48483 9bfb6978eb80
equal deleted inserted replaced
48474:5b9d79c6323b 48475:02dd825f5a4e
       
     1 session LCF! in "." = Pure +
       
     2   description {*
       
     3     Author:     Tobias Nipkow
       
     4     Copyright   1992  University of Cambridge
       
     5   *}
       
     6   theories LCF
       
     7 
       
     8 session ex = LCF +
       
     9   description {*
       
    10     Author:     Tobias Nipkow
       
    11     Copyright   1991  University of Cambridge
       
    12 
       
    13     Some examples from Lawrence Paulson's book Logic and Computation.
       
    14   *}
       
    15   theories Ex1 Ex2 Ex3 Ex4
       
    16