
**************************************
date: Thursday, September 30, 1993 @ 11:30
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/u1

Added Files:
	Makefile 
Log Message:
Added the Makefile for the u1 tactics.


    RCS Version:	1.1	/homes/itp/ver4/u1/Makefile,v

**************************************
date: Friday, October 1, 1993 @ 12:25
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	abbv.ql arith_dp.ql browse.ql conj.ql demo3.ql heur.ql 
	induction.ql it.ql lambda.ql mark1.ql quant.ql quick.ql 
	rerun.ql rt.ql search.ql show.ql std_heur.ql tools.ql 
	translate.ql 
Log Message:
Ran ~marku/bin/sicstus.update script over all the files.


    RCS Version:	1.2	/homes/itp/ver4/u1/abbv.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/arith_dp.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/conj.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/induction.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/it.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/lambda.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/quant.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/quick.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/std_heur.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/tools.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Tuesday, October 5, 1993 @ 14:22
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	abbv.ql arith_dp.ql back.ql browse.ql consult2.ql dbms_int.ql 
	demo3.ql forwards.ql heur.ql induction.ql int.ql it.ql 
	mark1.ql newuse.ql prinz.ql quick.ql rerun.ql rt.ql search.ql 
	show.ql startup.ql std_heur.ql systac.ql tools.ql translate.ql 
Log Message:
Keith's changes to the tactics, for the new compiler.


    RCS Version:	1.3	/homes/itp/ver4/u1/abbv.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/arith_dp.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/consult2.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/dbms_int.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/forwards.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/induction.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/int.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/it.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/prinz.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/quick.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/startup.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/std_heur.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/systac.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/tools.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Tuesday, October 5, 1993 @ 16:51
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	Makefile abbv.ql back.ql browse.ql buildthy.ql conj.ql 
	demo3.ql exprabbr.ql heur.ql int.ql it.ql localness.ql 
	mark1.ql newuse.ql prinz.ql quick.ql rerun.ql search.ql 
	show.ql startup.ql std_heur.ql systac.ql tactics.ql tools.ql 
	translate.ql 
Log Message:
Finished making changes for the new compiler.


    RCS Version:	1.2	/homes/itp/ver4/u1/Makefile,v
    RCS Version:	1.4	/homes/itp/ver4/u1/abbv.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/buildthy.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/conj.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/exprabbr.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/int.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/it.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/localness.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/prinz.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/quick.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/startup.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/std_heur.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/systac.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/tactics.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/tools.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Wednesday, October 6, 1993 @ 15:20
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	back.ql conj.ql heur.ql induction.ql int.ql it.ql mark1.ql 
	prinz.ql show.ql std_heur.ql tactics.ql 
Added Files:
	rewrite.ql 
Log Message:
Changed the way tactics are declared, to incorporate documentation.

Rewrote show so that the help message is database-driven, rather than
hard-coded and so that some output is pretty printed (esp. tactic,
heuristic, envir outputs).  The 'all' option works now.

Added some new rewrite tactics: rewrite/1 and rewrite/2 take a list
of rules to use for rewriting, while rewrite_group/1 and rewrite_group/2
take a rule_group name.


    RCS Version:	1.1	/homes/itp/ver4/u1/rewrite.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/conj.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/induction.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/int.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/it.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/prinz.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/std_heur.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/tactics.ql,v

**************************************
date: Thursday, October 7, 1993 @ 10:13
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	Makefile 
Log Message:
Fixed the Makefile to handle RCS files and added rewrite.ql.


    RCS Version:	1.3	/homes/itp/ver4/u1/Makefile,v

**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Thursday, October 7, 1993 @ 17:15
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/mark/u1

Modified Files:
	heur.ql search.ql show.ql 
Log Message:
Fixed a once bug in search and a typo in the envir/1 command.



**************************************
date: Friday, October 8, 1993 @ 11:38
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	Makefile 
Log Message:
Trivial change to test CVS file ownerships.


    RCS Version:	1.4	/homes/itp/ver4/u1/Makefile,v

**************************************
date: Friday, October 8, 1993 @ 13:32
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	rt.ql translate.ql 
Log Message:


Using inherited_symbol/3, is_theorem2 performs a restricted search for
theorem_hood relying on the fact that a theorem's theory must inherit
at least the outermost symbol of the theorem's statement.

term_theory/2 makes further use of inherited_symbol/3, and should be of
use to search queries like 'part contains ...'

satisfy/2 modified to use is_theorem2/2.




    RCS Version:	1.4	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Monday, October 11, 1993 @ 11:09
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	search.ql 
Log Message:
Added a speed-up optimisation to search for *= and contains queries.
They now should only search theories in which the given term is legal.
However, if a explicit theory=List condition is given, it overrides
this optimisation.


    RCS Version:	1.6	/homes/itp/ver4/u1/search.ql,v

**************************************
date: Monday, October 11, 1993 @ 14:20
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	search.ql 
Log Message:
Fixed a minor bug in search/2 so that tabs and newlines appear in the output.


    RCS Version:	1.7	/homes/itp/ver4/u1/search.ql,v

**************************************
date: Monday, October 11, 1993 @ 15:43
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	rt.ql 
Log Message:
Bugfix for is_theorem2



    RCS Version:	1.5	/homes/itp/ver4/u1/rt.ql,v

**************************************
date: Monday, October 11, 1993 @ 16:28
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	mark1.ql tools.ql 
Added Files:
	fol.ql 
Log Message:
eq_sub in fol.ql - like open_path but using substitutivity of equality.
rev_sub experimentally generalized to term (ie produce [Term/x]*Term =
Original)




    RCS Version:	1.1	/homes/itp/ver4/u1/fol.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/tools.ql,v

**************************************
date: Thursday, October 14, 1993 @ 10:08
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	newuse.ql 
Log Message:
Fixed another 'once' typo that was preventing use/3 from working.
Reported by alena.


    RCS Version:	1.4	/homes/itp/ver4/u1/newuse.ql,v

**************************************
date: Friday, October 15, 1993 @ 13:56
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	tactics.ql 
Log Message:
Fixed deny_focus.


    RCS Version:	1.4	/homes/itp/ver4/u1/tactics.ql,v

**************************************
date: Friday, October 15, 1993 @ 17:27
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	heur.ql 
Log Message:
Removed some of the unnecessary blank lines caused by heuristics.


    RCS Version:	1.7	/homes/itp/ver4/u1/heur.ql,v

**************************************
date: Friday, October 15, 1993 @ 17:28
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	int.ql 
Log Message:
Added some cuts in int/nat_induction tactics to remove excessive backtracking.


    RCS Version:	1.5	/homes/itp/ver4/u1/int.ql,v

**************************************
date: Monday, October 18, 1993 @ 10:09
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	back.ql demo3.ql heur.ql quant.ql rerun.ql show.ql std_heur.ql 
	tactics.ql 
Log Message:
Brought tactic descriptions into line with one another

Introduced 'multiple clause' heuristics, but I don't think these
will be around for long.

Imported quant.ql from demo3.3

Introduced 'safe_hyps' (previously a flag set by rerun), which should
override the automatic deletion of hypotheses by h_trans and open_pos.







    RCS Version:	1.5	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/quant.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/std_heur.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/tactics.ql,v

**************************************
date: Monday, October 18, 1993 @ 11:25
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Added Files:
	prop_auto.ql 
Log Message:
Initial and no doubt buggy version of propositional tautology checker

Initial version of predicate-logic clever thing.



    RCS Version:	1.1	/homes/itp/ver4/u1/prop_auto.ql,v

**************************************
date: Monday, October 18, 1993 @ 13:11
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	lambda.ql 
Log Message:
Quoted the argument to object_var to avoid spurious warnings.


    RCS Version:	1.3	/homes/itp/ver4/u1/lambda.ql,v

**************************************
date: Tuesday, October 19, 1993 @ 14:17
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	Makefile heur.ql newuse.ql rewrite.ql tools.ql 
Log Message:
Added a new way of printing messages for tactics (msg/2)
which allows the user/tactics to control the level of verbosity,
via the set_verbosity/2 and less_verbose/{1,2} commands.
Rewrote rewrite_group extensively to be standalone.


    RCS Version:	1.5	/homes/itp/ver4/u1/Makefile,v
    RCS Version:	1.9	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/rewrite.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/tools.ql,v

**************************************
date: Tuesday, October 19, 1993 @ 14:27
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	back.ql prop_auto.ql std_heur.ql 
Log Message:
Minor fixes



    RCS Version:	1.6	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/prop_auto.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/std_heur.ql,v

**************************************
date: Wednesday, October 20, 1993 @ 12:39
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	rt.ql 
Log Message:
Fixed a typo in term_theory:  quantifier --> quantify.


    RCS Version:	1.6	/homes/itp/ver4/u1/rt.ql,v

**************************************
date: Tuesday, October 26, 1993 @ 15:07
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	back.ql mark1.ql prinz.ql prop_auto.ql rerun.ql std_heur.ql 
Log Message:
Many minor changes

{dont_}save_proof/0  (For Andreas)



    RCS Version:	1.7	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/prinz.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/prop_auto.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/std_heur.ql,v

**************************************
date: Thursday, October 28, 1993 @ 16:05
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	demo3.ql 
Log Message:
Added rule_group/4 so that it is possible to add conditional
rules to a rule group in a less ambiguous way.


    RCS Version:	1.6	/homes/itp/ver4/u1/demo3.ql,v

**************************************
date: Friday, October 29, 1993 @ 9:18
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	translate.ql 
Log Message:
Changed absolute_function to generate is_local axioms:
    eg.  (is_local x Arg1) and ... => (is_local x f(Arg1,...)).
rather than localplaces axioms which used '='.


    RCS Version:	1.6	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Friday, October 29, 1993 @ 9:23
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	heur.ql newuse.ql rewrite.ql tools.ql 
Log Message:
Removed the first (tactic name) argument from msg/2.
Added the rewrite_subterm tactic (written by Ray).


    RCS Version:	1.10	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/rewrite.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/tools.ql,v

**************************************
date: Friday, October 29, 1993 @ 9:25
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	rewrite.ql 
Log Message:
Oops!  Fixed a missing quote in a tactic declaration.


    RCS Version:	1.4	/homes/itp/ver4/u1/rewrite.ql,v

**************************************
date: Friday, October 29, 1993 @ 11:19
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	demo3.ql 
Log Message:
Declared rule_group/4.


    RCS Version:	1.7	/homes/itp/ver4/u1/demo3.ql,v

**************************************
date: Tuesday, November 2, 1993 @ 14:56
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	translate.ql 
Log Message:
Made the parsing of function definitions more deterministic,
so that it doesn't try to declare the 'nonassoc' function upon failure!


    RCS Version:	1.7	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Thursday, November 4, 1993 @ 12:26
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	it.ql 
Log Message:
Changed proof prompt to show when you are inside a hypothesis.


    RCS Version:	1.6	/homes/itp/ver4/u1/it.ql,v

**************************************
date: Friday, November 5, 1993 @ 11:14
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	demo3.ql prinz.ql prop_auto.ql tools.ql 
Log Message:
Removed the old hyp/3 command and replaced calls to it by is_hyp.
Added the use_ex tactic.


    RCS Version:	1.8	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/prinz.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/prop_auto.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/tools.ql,v

**************************************
date: Friday, November 5, 1993 @ 13:24
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Added Files:
	int_simp.ql li_prove.ql 
Log Message:
Added Alena Griffith's Linear Arithmetic Tactics.


    RCS Version:	1.1	/homes/itp/ver4/u1/int_simp.ql,v
    RCS Version:	1.1	/homes/itp/ver4/u1/li_prove.ql,v

**************************************
date: Friday, November 5, 1993 @ 13:25
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	Makefile 
Log Message:
Added int_simp.ql and li_prove.ql to the Makefile


    RCS Version:	1.6	/homes/itp/ver4/u1/Makefile,v

**************************************
date: Monday, November 8, 1993 @ 11:52
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	conj.ql 
Log Message:
Extended conjuncts so that it does not require all conjuncts to be
transformed to true.  Now it succeeds iff at least one conjunct is
transformed in some way or a 'true' conjunct is removed.


    RCS Version:	1.5	/homes/itp/ver4/u1/conj.ql,v

**************************************
date: Wednesday, November 10, 1993 @ 14:30
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	browse.ql demo3.ql rerun.ql rt.ql tools.ql 
Log Message:
Added conjecture/discharge mechanism

	- Rerun will update older (1.2) proofs to new format,
	  and will rerun new proofs containing conjectures

	- Conjectures and their dependants marked with '?' and '%' 
	  in window printouts

	- Browse is still pretty buggy





    RCS Version:	1.5	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/tools.ql,v

**************************************
date: Thursday, November 11, 1993 @ 14:51
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	demo3.ql 
Log Message:
Made rule_group/3 a little more smart for ambiguous directions.


    RCS Version:	1.10	/homes/itp/ver4/u1/demo3.ql,v

**************************************
date: Friday, November 12, 1993 @ 13:07
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	browse.ql demo3.ql it.ql rerun.ql tools.ql 
Log Message:

Fixes to hyp splitting where conjectures are involved.

quit gives a message if you try to leave an unjustified window,

really_quit  allows this



    RCS Version:	1.6	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/it.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/tools.ql,v

**************************************
date: Friday, November 12, 1993 @ 17:11
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	li_prove.ql 
Log Message:
Made the li_prove tactic more deterministic.


    RCS Version:	1.2	/homes/itp/ver4/u1/li_prove.ql,v

**************************************
date: Friday, November 12, 1993 @ 17:13
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	it.ql 
Log Message:
Replaced some once(_) calls by cuts.


    RCS Version:	1.8	/homes/itp/ver4/u1/it.ql,v

**************************************
date: Friday, November 12, 1993 @ 17:13
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	commands1.ql 
Log Message:
Declared the new commands for compiled rules.


    RCS Version:	1.2	/homes/itp/ver4/u1/commands1.ql,v

**************************************
date: Friday, November 12, 1993 @ 17:16
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	demo3.ql 
Log Message:
Changed the automatic simplification routine to look for
simplification rules in a more efficient way (specifying the group name).
Rewrote rule_group/4 to remove some failure cases.
It now uses the choose_conditional/choose_direction procedures from trans.ql.


    RCS Version:	1.12	/homes/itp/ver4/u1/demo3.ql,v

**************************************
date: Friday, November 12, 1993 @ 17:18
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	heur.ql 
Log Message:
Modified nth1 to match standard Prolog (and arg/3).


    RCS Version:	1.11	/homes/itp/ver4/u1/heur.ql,v

**************************************
date: Friday, November 12, 1993 @ 18:02
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	std_heur.ql 
Log Message:
Changed the 'quit' heuristic to check that no outstanding conjectures
are in the current window before it decides to quit.


    RCS Version:	1.9	/homes/itp/ver4/u1/std_heur.ql,v

**************************************
date: Monday, November 15, 1993 @ 15:31
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	conj.ql 
Log Message:
Rewrote conjuncts yet again.  It now performs simplification of true
conjuncts a little earlier, which avoids the 'true' hypotheses that
used to occur.


    RCS Version:	1.6	/homes/itp/ver4/u1/conj.ql,v

**************************************
date: Monday, November 15, 1993 @ 15:32
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	mark1.ql 
Log Message:
Added a 'false' tactic, which searches for a rule of the form: not Focus
then uses that rule to transform the focus to false.


    RCS Version:	1.8	/homes/itp/ver4/u1/mark1.ql,v

**************************************
date: Monday, November 15, 1993 @ 16:40
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	mark1.ql 
Log Message:
Fixed missing comma in false tactic...


    RCS Version:	1.9	/homes/itp/ver4/u1/mark1.ql,v

**************************************
date: Monday, November 15, 1993 @ 17:04
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	exprabbr.ql 
Log Message:
Extended abbreviations so that given input A and B and C, if B expands to
a conjunction, B1 and B2, the result is A and (B1 and (B2 and C)), rather
than the usual A and ((B1 and B2) and C).  This makes abbreviations
more useful within lists of conjuncts (esp. antecedent lists).


    RCS Version:	1.3	/homes/itp/ver4/u1/exprabbr.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 15:42
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	abbv.ql arith_dp.ql back.ql browse.ql buildthy.ql commands1.ql 
	commands2.ql conj.ql consult2.ql dbms_int.ql demo3.ql 
	exprabbr.ql fol.ql forwards.ql heur.ql induction.ql int.ql 
	int_simp.ql it.ql lambda.ql li_prove.ql localness.ql mark1.ql 
	newuse.ql prinz.ql prop_auto.ql quant.ql quick.ql rerun.ql 
	rewrite.ql rt.ql search.ql show.ql startup.ql std_heur.ql 
	systac.ql tactics.ql tools.ql translate.ql 
Log Message:
Added copyright message and CVS $Id:$ line.
Also, extended search/2 to handle compiled rules.


    RCS Version:	1.5	/homes/itp/ver4/u1/abbv.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/arith_dp.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/buildthy.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/commands1.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/commands2.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/conj.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/consult2.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/dbms_int.ql,v
    RCS Version:	1.13	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/exprabbr.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/fol.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/forwards.ql,v
    RCS Version:	1.12	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/induction.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/int.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/int_simp.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/it.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/lambda.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/li_prove.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/localness.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/prinz.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/prop_auto.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/quant.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/quick.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/rewrite.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/startup.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/std_heur.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/systac.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/tactics.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/tools.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 17:05
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	search.ql 
Log Message:
Fixed a syntax bug.


    RCS Version:	1.9	/homes/itp/ver4/u1/search.ql,v

**************************************
date: Friday, November 19, 1993 @ 10:31
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	Makefile 
Log Message:
Changed qc path to /homes/qp/qp3.2/qc.


    RCS Version:	1.7	/homes/itp/ver4/u1/Makefile,v

**************************************
date: Friday, November 19, 1993 @ 15:03
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	Makefile 
Log Message:
Tidied up Makefile and moved system specific paths to the top.


    RCS Version:	1.8	/homes/itp/ver4/u1/Makefile,v

**************************************
date: Friday, November 19, 1993 @ 15:07
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	demo3.ql 
Log Message:
Changed the focus command (do_simplifications actually) so that it does
not attempt to perform simplifications when the focus is atomic or
a variable.  This should speed up opening/closing of such windows.


    RCS Version:	1.14	/homes/itp/ver4/u1/demo3.ql,v

**************************************
date: Friday, November 19, 1993 @ 15:13
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	translate.ql exprabbr.ql 
Log Message:
Removed the duplicated RCS $Id:...$ lines.


    RCS Version:	1.9	/homes/itp/ver4/u1/translate.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/exprabbr.ql,v

**************************************
date: Friday, November 19, 1993 @ 15:15
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	newuse.ql rt.ql search.ql 
Log Message:
Reimplemented use and fwd to use conjectures.
Also, defined satisfy/3, which can generate conjectures for
any conditions that cannot be satisfied in other ways.


    RCS Version:	1.8	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/search.ql,v

**************************************
date: Monday, November 22, 1993 @ 16:03
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	rt.ql search.ql 
Log Message:
Pushed the 'is_theorem2' type search restrictions into
find_rule etc

Reflect this in new code for is_theorem2 (of course) and search




    RCS Version:	1.10	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/search.ql,v

**************************************
date: Monday, November 22, 1993 @ 18:13
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	fol.ql 
Log Message:

eq_pos uses conjecture rather than new_hyp



    RCS Version:	1.3	/homes/itp/ver4/u1/fol.ql,v

**************************************
date: Tuesday, November 23, 1993 @ 14:25
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	li_prove.ql rewrite.ql search.ql show.ql std_heur.ql 
Log Message:
Removed the rewrite* tactics that took an environment argument.
Added the discharge_hyp heuristic, which calls discharge_hyp
whenever the focus depends upon conjectures.
Added show(theory) to the show command.


    RCS Version:	1.4	/homes/itp/ver4/u1/li_prove.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/rewrite.ql,v
    RCS Version:	1.12	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/std_heur.ql,v

**************************************
date: Tuesday, November 23, 1993 @ 15:38
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	rt.ql 
Log Message:
Fixed minor typo in is_theorem2


    RCS Version:	1.11	/homes/itp/ver4/u1/rt.ql,v

**************************************
date: Thursday, November 25, 1993 @ 12:49
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	commands1.ql 
Log Message:
Added the compiled_rulez commands.


    RCS Version:	1.4	/homes/itp/ver4/u1/commands1.ql,v

**************************************
date: Thursday, November 25, 1993 @ 12:51
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	int.ql 
Log Message:
Added more heuristics for arithmetic, plus the 'arith' environment.
Made this 'arith' environment the default for arithmetic theories.


    RCS Version:	1.7	/homes/itp/ver4/u1/int.ql,v

**************************************
date: Friday, November 26, 1993 @ 13:34
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Modified Files:
	browse.ql commands1.ql search.ql startup.ql translate.ql 
Log Message:
Changed 'name' to 'atom_chars' throughout - name does strange
	stuff when arg 2 is nonvar.

Changed 'reverse' to (new) 'rev_tr' 
	- reverse in qp libraries is the naive version!

Added 'Implicit Parameter' dbms commands
	Most obvious example of such a command is 'envir/1',
	
	These commands are undo-able.  An undo at the dbms prompt
	ie [r] : 
	refers to the last ip_command executed.




    RCS Version:	1.8	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/commands1.ql,v
    RCS Version:	1.13	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/startup.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Monday, November 29, 1993 @ 10:44
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	newuse.ql rt.ql 
Log Message:
Changed fwd to avoid 'rt' directions for compiled rules.
Instead it adds a conjecture, then uses the 't' direction.


    RCS Version:	1.9	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.12	/homes/itp/ver4/u1/rt.ql,v

**************************************
date: Tuesday, November 30, 1993 @ 16:47
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	search.ql newuse.ql 
Log Message:
Extended search/2 etc. to check that the conclusion contains a known preorder.
Fixed some bugs in use and fwd and extended them to recognise special
outputs such as 'focus', 'goal' and h(N).


    RCS Version:	1.14	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/newuse.ql,v

**************************************
date: Tuesday, November 30, 1993 @ 16:49
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	std_heur.ql 
Log Message:
Added the 'localness' heuristic.
Changed the 'when' heuristic so that it doesn't instantiate its first arg.


    RCS Version:	1.12	/homes/itp/ver4/u1/std_heur.ql,v

**************************************
date: Wednesday, December 8, 1993 @ 14:20
author: itp
Update of /homes/itp/ver4/u1
In directory everest:/u1/everest/itp/keith/u1

Added Files:
	kcompare.ql 
Log Message:
Experimental term comparision for the arithmetic simpifier.




    RCS Version:	1.1	/homes/itp/ver4/u1/kcompare.ql,v

**************************************
date: Thursday, December 9, 1993 @ 17:08
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	int.ql li_prove.ql 
Log Message:
Changed nat_induction to reflect the new nat_induction2 rule.
(It selects automatically between it and nat_induction).
Made some minor (temporary) improvements to the linear_comb stage of li_prove.


    RCS Version:	1.8	/homes/itp/ver4/u1/int.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/li_prove.ql,v

**************************************
date: Thursday, December 9, 1993 @ 18:04
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	rerun.ql 
Log Message:
Fixed browse and rerun to handle lib(_) paths.


    RCS Version:	1.10	/homes/itp/ver4/u1/rerun.ql,v

**************************************
date: Friday, December 10, 1993 @ 12:19
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	abbv.ql arith_dp.ql back.ql browse.ql buildthy.ql commands1.ql 
	commands2.ql conj.ql consult2.ql dbms_int.ql demo3.ql 
	exprabbr.ql fol.ql forwards.ql heur.ql induction.ql int.ql 
	int_simp.ql it.ql kcompare.ql lambda.ql li_prove.ql 
	localness.ql mark1.ql newuse.ql prinz.ql prop_auto.ql quant.ql 
	quick.ql rerun.ql rewrite.ql rt.ql search.ql show.ql 
	startup.ql std_heur.ql systac.ql tactics.ql tools.ql 
	translate.ql 
Log Message:
Updated-Copyright

    RCS Version:	1.6	/homes/itp/ver4/u1/abbv.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/arith_dp.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/back.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/browse.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/buildthy.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/commands1.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/commands2.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/conj.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/consult2.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/dbms_int.ql,v
    RCS Version:	1.15	/homes/itp/ver4/u1/demo3.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/exprabbr.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/fol.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/forwards.ql,v
    RCS Version:	1.13	/homes/itp/ver4/u1/heur.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/induction.ql,v
    RCS Version:	1.9	/homes/itp/ver4/u1/int.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/int_simp.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/it.ql,v
    RCS Version:	1.2	/homes/itp/ver4/u1/kcompare.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/lambda.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/li_prove.ql,v
    RCS Version:	1.4	/homes/itp/ver4/u1/localness.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/mark1.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/newuse.ql,v
    RCS Version:	1.8	/homes/itp/ver4/u1/prinz.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/prop_auto.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/quant.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/quick.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/rerun.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/rewrite.ql,v
    RCS Version:	1.13	/homes/itp/ver4/u1/rt.ql,v
    RCS Version:	1.15	/homes/itp/ver4/u1/search.ql,v
    RCS Version:	1.10	/homes/itp/ver4/u1/show.ql,v
    RCS Version:	1.6	/homes/itp/ver4/u1/startup.ql,v
    RCS Version:	1.13	/homes/itp/ver4/u1/std_heur.ql,v
    RCS Version:	1.5	/homes/itp/ver4/u1/systac.ql,v
    RCS Version:	1.7	/homes/itp/ver4/u1/tactics.ql,v
    RCS Version:	1.12	/homes/itp/ver4/u1/tools.ql,v
    RCS Version:	1.11	/homes/itp/ver4/u1/translate.ql,v

**************************************
date: Friday, December 10, 1993 @ 12:21
author: marku
Update of /homes/itp/ver4/u1
In directory everest:/u0/everest/marku/Ergo/u1

Modified Files:
	fol.ql kcompare.ql 
Log Message:
Updated-Copyright

    RCS Version:	1.5	/homes/itp/ver4/u1/fol.ql,v
    RCS Version:	1.3	/homes/itp/ver4/u1/kcompare.ql,v
