src/HOL/README.html
changeset 3125 3f0ab2c306f7
parent 2080 12eed4cec935
child 3279 815ef5848324
--- a/src/HOL/README.html	Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/README.html	Wed May 07 13:51:22 1997 +0200
@@ -31,11 +31,14 @@
 <DT>IMP
 <DD>mechanization of a large part of a semantics text by Glynn Winskel
 
+<DT>Induct
+<DD>examples of (co)inductive definitions
+
 <DT>Integ
 <DD>a theory of the integers including efficient integer calculations
 
 <DT>IOA
-<DD>extended example of Input/Output Automata (takes a long time to run!)
+<DD>extended example of Input/Output Automata
 
 <DT>Lambda
 <DD>a proof of the Church-Rosser theorem for lambda-calculus