Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 18 Aug 1994 21:25:18 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02687;
          Thu, 18 Aug 1994 14:18:37 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from scapa.cs.ualberta.ca by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA02683;
          Thu, 18 Aug 1994 14:18:36 -0600
Received: from tees.cs.ualberta.ca by scapa.cs.ualberta.ca id <18454-2>;
          Thu, 18 Aug 1994 14:14:24 -0600
Subject: A question
From: Miroslava Kaloper <kaloper@cs.ualberta.ca>
To: info-hol@leopard.cs.byu.edu
Date: Thu, 18 Aug 1994 14:14:18 -0600
X-Mailer: ELM [version 2.4 PL23]
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 238
Message-Id: <94Aug18.141424mdt.18454-2@scapa.cs.ualberta.ca>

Hi:
 
I am finishing my master thesis on the 
minimization theorem for finite state
machines in the Mizar proof system.
I would like to know if something similar has 
been done in HOL. Any references would 
be appreciated.

Thanks, Mira