Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: marco@mirtillo.usr.dsi.unimi.it (Marco Benini)
Message-Id: <9507190207.AA01330@ mirtillo.usr.dsi.unimi.it >
Subject: easy HOL?
To: info-hol@cs.uidaho.edu
Date: Tue, 18 Jul 1995 19:07:39 -0700 (PDT)
Cc: shepherd_david/uk_bristo_br@brx001.bristol.st.com
In-Reply-To: stol.st.com521c02@MHS> from "shepherd_david/uk_bristo_br@brx001.bristol.st.com" at Jul 18, 95 10:15:35 am
Content-Type: text
Content-Length: 1245

I know it is a "bad" thing to rely on assumptions ordering.

The point I wanted to show with my posting was that a good
way to improve ability of a novice user is to give him simple
tactics to do simple works he feels "natural".

This kind of tactics is good for a "startup" package, the
novice HOLer may use to approach theorem proving. Obviously,
because of their inelegance, inefficiency, non-portability,
etc., they are strongly discouraged to normal users. But, 
in the meantime, novices can (should) learn good way to do
things.

This is my opinion: to give new users a quick and dirty way
to get results. Their leaning curve will be slow, but they
will be able to get results quickly. Perhaps this helps.

I would like to hear opinions on this approach.

	Marco

-----------------------------------------------------------
Marco Benini			marco@mora.usr.dsi.unimi.it
   Departement of Computer Science - University of Milan
           Computational Architectures Laboratory
tel. 0039-02-55006344		      fax. 0039-02-55006348
-----------------------------------------------------------

"But did thee feel the earth move?"
For Whom the Bell Tolls (1940), ch.13, ERNEST HEMINGWAY

GCS/M d-- -p+ c++ l+ u+ e--- m++ s/- !n h* f+ g+ w+ t r+ y+