src/HOL/README.html
changeset 3125 3f0ab2c306f7
parent 2080 12eed4cec935
child 3279 815ef5848324
equal deleted inserted replaced
3124:1c0dfa7ebb72 3125:3f0ab2c306f7
    29 <DD>a new approach to verifying authentication protocols 
    29 <DD>a new approach to verifying authentication protocols 
    30 
    30 
    31 <DT>IMP
    31 <DT>IMP
    32 <DD>mechanization of a large part of a semantics text by Glynn Winskel
    32 <DD>mechanization of a large part of a semantics text by Glynn Winskel
    33 
    33 
       
    34 <DT>Induct
       
    35 <DD>examples of (co)inductive definitions
       
    36 
    34 <DT>Integ
    37 <DT>Integ
    35 <DD>a theory of the integers including efficient integer calculations
    38 <DD>a theory of the integers including efficient integer calculations
    36 
    39 
    37 <DT>IOA
    40 <DT>IOA
    38 <DD>extended example of Input/Output Automata (takes a long time to run!)
    41 <DD>extended example of Input/Output Automata
    39 
    42 
    40 <DT>Lambda
    43 <DT>Lambda
    41 <DD>a proof of the Church-Rosser theorem for lambda-calculus
    44 <DD>a proof of the Church-Rosser theorem for lambda-calculus
    42 
    45 
    43 <DT>Subst
    46 <DT>Subst