
**************************************
date: Friday, October 1, 1993 @ 13:31
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/mark/prover/dbms

Modified Files:
	assert.ql fact_types.ql main.ql query.ql syntax1.ql syntax2.ql 
	theory_dag.ql theory_data.ql unix.ql win_rule.ql 
Log Message:
Ran all files through ~marku/bin/sicstus.update, for the new compiler.


    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/assert.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/fact_types.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/main.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/syntax1.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/syntax2.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/theory_dag.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/theory_data.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/unix.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/win_rule.ql,v

**************************************
date: Friday, October 1, 1993 @ 13:32
author: itp
Update of /homes/itp/ver4/prover/lib
In directory everest:/u1/everest/itp/mark/prover/lib

Modified Files:
	arith.ql io.ql macros.ql tools.ql unif.ql 
Log Message:
Ran all files through ~marku/bin/sicstus.update, for the new compiler.


    RCS Version:	1.2	/homes/itp/ver4/prover/lib/arith.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/lib/io.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/lib/macros.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/lib/tools.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/lib/unif.ql,v

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

Modified Files:
	hyps.ql newvars.ql prove.ql trans.ql window.ql 
Log Message:
Ran all files through ~marku/bin/sicstus.update, for the new compiler.


    RCS Version:	1.2	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/prover/window.ql,v

**************************************
date: Friday, October 1, 1993 @ 16:04
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/mark/prover/dbms

Modified Files:
	assert.ql main.ql syntax1.ql syntax2.ql theory_dag.ql 
	theory_data.ql unix.ql win_rule.ql 
Log Message:
Changed syntax for new Qu-Prolog compiler.


    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/assert.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/main.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/syntax1.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/syntax2.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/theory_dag.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/theory_data.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/unix.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/win_rule.ql,v

**************************************
date: Friday, October 1, 1993 @ 16:04
author: itp
Update of /homes/itp/ver4/prover/lib
In directory everest:/u1/everest/itp/mark/prover/lib

Modified Files:
	arith.ql io.ql macros.ql unif.ql 
Log Message:
Changed syntax for new Qu-Prolog compiler.


    RCS Version:	1.3	/homes/itp/ver4/prover/lib/arith.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/lib/io.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/lib/macros.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/lib/unif.ql,v

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

Modified Files:
	hyps.ql newvars.ql prove.ql take_thm.ql trans.ql window.ql 
Log Message:
Changed syntax for new Qu-Prolog compiler.


    RCS Version:	1.3	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/prover/take_thm.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/prover/window.ql,v

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

Modified Files:
	Makefile 
Log Message:
Changed the Makefile so that the release version looks for data files
in /homes/itp/Ergo/thy (which will be a release copy of /homes/itp/ver4/thy)
and looks for the u1 tactics in /homes/itp/ver4/u1 (the master sources).


    RCS Version:	1.2	/homes/itp/ver4/prover/Makefile,v

**************************************
date: Wednesday, October 6, 1993 @ 16:24
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/mark/prover/dbms

Modified Files:
	assert.ql query.ql syntax1.ql syntax2.ql theory_dag.ql 
	theory_data.ql unix.ql 
Log Message:
Removed all embedded \t and \n's, due to compiler change.


    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/assert.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/syntax1.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/syntax2.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/theory_dag.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/theory_data.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/unix.ql,v

**************************************
date: Wednesday, October 6, 1993 @ 16:29
author: itp
Update of /homes/itp/ver4/prover/lib
In directory everest:/u1/everest/itp/mark/prover/lib

Modified Files:
	development.ql release.ql 
Log Message:
Removed all embedded \t and \n's, due to compiler change.
Also turned the frozen_nfi_test flag on during the execution of
rule bodies within 'trans' commands.  This should mean that trans
cannot add not_free_in conditions on frozen variables.


    RCS Version:	1.2	/homes/itp/ver4/prover/lib/development.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/lib/release.ql,v

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

Modified Files:
	prove.ql trans.ql 
Log Message:
Removed all embedded \t and \n's, due to compiler change.
Also turned the frozen_nfi_test flag on during the execution of
rule bodies within 'trans' commands.  This should mean that trans
cannot add not_free_in conditions on frozen variables.


    RCS Version:	1.4	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/prover/trans.ql,v

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

Modified Files:
	Makefile 
Log Message:
Fixed the Makefile to handle RCS sources.


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

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

Modified Files:
	syntax1.ql syntax2.ql theory_dag.ql 
Log Message:
Expanded inherited_symbol to /3, the third argument reflecting the
currently inherited symbols which inherit the symbol.

mk_child_lists/0 compiles a table of the active children of each currently
inherited theory.




    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/syntax1.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/syntax2.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

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

Modified Files:
	Makefile 
Log Message:
Changed the names of the stored theory files from .dyl to .erg.
Similarly, the global file is now called 'global.erg'.

Extended writelist to handle 'tab' and 'tab(N)' terms as special.
Added some optimisations to search/2 using the new term_theory/2.


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

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

Modified Files:
	main.ql save.ql unix.ql 
Log Message:
Changed the names of the stored theory files from .dyl to .erg.
Similarly, the global file is now called 'global.erg'.

Extended writelist to handle 'tab' and 'tab(N)' terms as special.
Added some optimisations to search/2 using the new term_theory/2.


    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/main.ql,v
    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/save.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	development.ql io.ql 
Log Message:
Changed the names of the stored theory files from .dyl to .erg.
Similarly, the global file is now called 'global.erg'.

Extended writelist to handle 'tab' and 'tab(N)' terms as special.
Added some optimisations to search/2 using the new term_theory/2.


    RCS Version:	1.3	/homes/itp/ver4/prover/lib/development.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/lib/io.ql,v

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

Modified Files:
	query.ql theory_dag.ql 
Log Message:
Bug fixes to mk_inherited_symbols, so that inherit_theory works.


    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

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

Modified Files:
	theory_dag.ql 
Log Message:
inherited symbols give theories in youngest first order



    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

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

Modified Files:
	io.ql 
Added Files:
	iu.ql 
Log Message:
New incomplete unifier



    RCS Version:	1.1	/homes/itp/ver4/prover/lib/iu.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/lib/io.ql,v

**************************************
date: Thursday, October 14, 1993 @ 13:16
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/keith/prover/dbms

Modified Files:
	theory_data.ql 
Log Message:
Fixed defq
.




    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/theory_data.ql,v

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

Modified Files:
	query.ql theory_dag.ql 
Log Message:
Small changes to is_theorem



    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

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

Modified Files:
	hyps.ql newvars.ql prove.ql take_thm.ql trans.ql window.ql 
Log Message:

Relaxed syntax-checking on trans & take_theorem
Fixed get_th_or_hyp to return fully specific rule descriptor




    RCS Version:	1.4	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/prover/take_thm.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/prover/window.ql,v

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

Modified Files:
	hyps.ql newvars.ql 
Log Message:
Fixed assimilate_new_vars




    RCS Version:	1.5	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/prover/newvars.ql,v

**************************************
date: Tuesday, October 19, 1993 @ 15:10
author: marku
Update of /homes/itp/ver4/prover
In directory everest:/u0/everest/marku/Ergo/prover

Modified Files:
	Makefile 
Log Message:
Changed the make commands for 'er' and 'ergo' to avoid ownership
problems by deleting them before making them.


    RCS Version:	1.5	/homes/itp/ver4/prover/Makefile,v

**************************************
date: Tuesday, October 19, 1993 @ 15:13
author: marku
Update of /homes/itp/ver4/prover/lib
In directory everest:/u0/everest/marku/Ergo/prover/lib

Modified Files:
	iu.ql 
Log Message:
Added complete_retry_delays.


    RCS Version:	1.2	/homes/itp/ver4/prover/lib/iu.ql,v

**************************************
date: Tuesday, October 19, 1993 @ 15:13
author: marku
Update of /homes/itp/ver4/prover/prover
In directory everest:/u0/everest/marku/Ergo/prover/prover

Modified Files:
	prove.ql 
Log Message:
Set the initial value of the verbosity flag to 1.


    RCS Version:	1.6	/homes/itp/ver4/prover/prover/prove.ql,v

**************************************
date: Wednesday, October 20, 1993 @ 9:10
author: marku
Update of /homes/itp/ver4/prover
In directory everest:/u0/everest/marku/Ergo/prover

Modified Files:
	Makefile 
Log Message:
Added a chmod to the make commands for 'er' and 'ergo' to ensure that
the resulting shell script is readable and executable by all.
Also, changed over to the new incomplete unify (iu.ql instead of unif.ql).


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

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

Modified Files:
	fact_types.ql unix.ql 
Log Message:
Ergo needs now to be primed with the command

help_cmd('ksh blah').

This is available only at the ?- prompt.



    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/fact_types.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	iu.ql 
Log Message:
Not me?



    RCS Version:	1.3	/homes/itp/ver4/prover/lib/iu.ql,v

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

Modified Files:
	prove.ql 
Log Message:
Syntactic changes



    RCS Version:	1.7	/homes/itp/ver4/prover/prover/prove.ql,v

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

Modified Files:
	fact_types.ql unix.ql 
Log Message:
Help command by command line argument

eg 

ergo -H ~itp/abc/d

(the ksh is assumed)





    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/fact_types.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	Makefile 
Log Message:
Help path again



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

**************************************
date: Friday, October 29, 1993 @ 17:00
author: marku
Update of /homes/itp/ver4/prover/prover
In directory everest:/u0/everest/marku/Ergo/prover/prover

Modified Files:
	prove.ql 
Log Message:
Removed declaration of <=>, because => is used instead now.


    RCS Version:	1.8	/homes/itp/ver4/prover/prover/prove.ql,v

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

Modified Files:
	prove.ql window.ql 
Log Message:
Fixed incrementing of window level when you go inside a hypothesis.


    RCS Version:	1.9	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/prover/window.ql,v

**************************************
date: Monday, November 8, 1993 @ 12:45
author: marku
Update of /homes/itp/ver4/prover/lib
In directory everest:/u0/everest/marku/Ergo/prover/lib

Modified Files:
	iu.ql 
Log Message:
Changed incomplete_retry_delays to write out delayed problems
in a more meaningful style.  (and, temporarily, without simplification!).


    RCS Version:	1.4	/homes/itp/ver4/prover/lib/iu.ql,v

**************************************
date: Tuesday, November 9, 1993 @ 15:54
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Added Files:
	comprule.ql 
Log Message:
Compiled Rules.


    RCS Version:	1.1	/homes/itp/ver4/prover/dbms/comprule.ql,v

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

Modified Files:
	hyps.ql newvars.ql prove.ql take_thm.ql trans.ql window.ql 
Log Message:
Added conjecture/discharge mechanism

	conjecture(+NewTerm, -HypNr)
	conjecture(+NewTerm)

	discharge(Hyp, Tactic)
	discharge_hyp(Hyp)

Added the concept of 'proofvars', such that
 
	proofvars + newvars = all_the_vars_in_the_proof

This makes saving the proof a lot quicker.





    RCS Version:	1.6	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.10	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/prover/take_thm.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/prover/window.ql,v

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

Modified Files:
	Makefile 
Log Message:
Switched to relative pathname for preloaded tatics



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

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

Modified Files:
	save.ql unix.ql 
Log Message:
Saving theory facts with processed clause names.  This speeds up
loading of theory files quite a bit.



    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/save.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	io.ql 
Log Message:



    RCS Version:	1.7	/homes/itp/ver4/prover/lib/io.ql,v

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

Modified Files:
	hyps.ql window.ql 
Log Message:

Fixes to hyp splitting where conjectures are involved.

added:  is_justified_window

which fails if  there is a hyp of the current window upon which the focus
depends



    RCS Version:	1.7	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/prover/window.ql,v

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

Modified Files:
	trans.ql 
Log Message:
Modified trans/9 to build a skeleton of the rule it expects.
Also, added three procedures that are useful elsewhere in Ergo.
    %% decode_direction(+Dirn0, +AntList, -Dirn).
    %% choose_conditional(?CondFlag, ?Form, ?Conds, ?Concl).
    %% choose_direction(?Direction, ?Concl, ?Input, ?RuleEq, ?Output).
The first of these returns a fully specified direction of the
form 'direction(C,D)', where C is 'u' or 'c' and D is 'f', 'r', 't' or 'rt'.


    RCS Version:	1.7	/homes/itp/ver4/prover/prover/trans.ql,v

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

Modified Files:
	Makefile 
Log Message:
Added compiled rules.

%% begin_compiled_rule(+Call, +Patt, +OptionList)
%%
%%   Declares a new compiled rule group that will be used
%%   to generate theorems of the form Patt.

%% end_compiled_rule(+Name).
%%
%%   This command completes the construction of the compiled rule 
%%   group called Name.  Once this command has been executed, no
%%   more rules can be added to the group.

%% get_compiled_rule(?Thy, ?Name, ?Call, ?Form)
%%
%%   This procedure gets the most commonly needed information about
%%   a compiled rule from the database, without evaluating the rule.

%% eval_compiled_rule(?Thy, ?Name, +Call, ?InForm, -FinalForm, -Deps).
%% eval_compiled_rule(?Thy, ?Name, ?Call, +InForm, -FinalForm, -Deps).
%% 
%%   This procedure attempts to generate a theorem
%%   that matches the specified arguments of Call and/or Form.
%%   If it succeeds, it instantiates Call and Form as well as
%%   returning the whole theorem in FinalForm.
%%   Deps is a list of dependency variables, to indicate which
%%   conjectures this compiled rule depends upon.


    RCS Version:	1.9	/homes/itp/ver4/prover/Makefile,v

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

Modified Files:
	comprule.ql fact_types.ql query.ql save.ql 
Log Message:
Added compiled rules.

%% begin_compiled_rule(+Call, +Patt, +OptionList)
%%
%%   Declares a new compiled rule group that will be used
%%   to generate theorems of the form Patt.

%% end_compiled_rule(+Name).
%%
%%   This command completes the construction of the compiled rule 
%%   group called Name.  Once this command has been executed, no
%%   more rules can be added to the group.

%% get_compiled_rule(?Thy, ?Name, ?Call, ?Form)
%%
%%   This procedure gets the most commonly needed information about
%%   a compiled rule from the database, without evaluating the rule.

%% eval_compiled_rule(?Thy, ?Name, +Call, ?InForm, -FinalForm, -Deps).
%% eval_compiled_rule(?Thy, ?Name, ?Call, +InForm, -FinalForm, -Deps).
%% 
%%   This procedure attempts to generate a theorem
%%   that matches the specified arguments of Call and/or Form.
%%   If it succeeds, it instantiates Call and Form as well as
%%   returning the whole theorem in FinalForm.
%%   Deps is a list of dependency variables, to indicate which
%%   conjectures this compiled rule depends upon.


    RCS Version:	1.2	/homes/itp/ver4/prover/dbms/comprule.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/fact_types.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/save.ql,v

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

Modified Files:
	hyps.ql trans.ql 
Log Message:
Added compiled rules.

%% begin_compiled_rule(+Call, +Patt, +OptionList)
%%
%%   Declares a new compiled rule group that will be used
%%   to generate theorems of the form Patt.

%% end_compiled_rule(+Name).
%%
%%   This command completes the construction of the compiled rule 
%%   group called Name.  Once this command has been executed, no
%%   more rules can be added to the group.

%% get_compiled_rule(?Thy, ?Name, ?Call, ?Form)
%%
%%   This procedure gets the most commonly needed information about
%%   a compiled rule from the database, without evaluating the rule.

%% eval_compiled_rule(?Thy, ?Name, +Call, ?InForm, -FinalForm, -Deps).
%% eval_compiled_rule(?Thy, ?Name, ?Call, +InForm, -FinalForm, -Deps).
%% 
%%   This procedure attempts to generate a theorem
%%   that matches the specified arguments of Call and/or Form.
%%   If it succeeds, it instantiates Call and Form as well as
%%   returning the whole theorem in FinalForm.
%%   Deps is a list of dependency variables, to indicate which
%%   conjectures this compiled rule depends upon.


    RCS Version:	1.8	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/prover/trans.ql,v

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

Modified Files:
	query.ql 
Log Message:
Strengthened stronger/2 to handle rev(E), where E is an equivalence.


    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/query.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 12:03
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	theory_dag.ql 
Log Message:
Added rev_of(rev(E), E) for equivalence relations E.


    RCS Version:	1.9	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 12:10
author: itp
Update of /homes/itp/ver4/prover/prover
In directory everest:/u1/everest/itp/keith/prover/prover

Modified Files:
	hyps.ql trans.ql window.ql 
Log Message:

New trans:

	Allows c(N) and c in antecedent list (and perhaps too many other
					      places besides)

	Faster syntax checking




    RCS Version:	1.9	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.9	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/prover/window.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 12:26
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/keith/prover/dbms

Modified Files:
	query.ql 
Log Message:
 
 Undoing an update anomaly



    RCS Version:	1.8	/homes/itp/ver4/prover/dbms/query.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 12:56
author: marku
Update of /homes/itp/ver4/prover/prover
In directory everest:/u0/everest/marku/Ergo/prover/prover

Modified Files:
	hyps.ql 
Log Message:
Reinstalled support for compiled rules within get_th_or_hyp.


    RCS Version:	1.10	/homes/itp/ver4/prover/prover/hyps.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 13:08
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	query.ql 
Log Message:
Reinstalled changes to stronger/2.


    RCS Version:	1.9	/homes/itp/ver4/prover/dbms/query.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 13:50
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/keith/prover/dbms

Modified Files:
	save.ql 
Log Message:
Modified save to cope with changes to qprolog



    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/save.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 15:34
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/keith/prover/dbms

Modified Files:
	query.ql theory_dag.ql 
Log Message:
New method for storing preorder information.



    RCS Version:	1.10	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.10	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

**************************************
date: Tuesday, November 16, 1993 @ 15:35
author: itp
Update of /homes/itp/ver4/prover/prover
In directory everest:/u1/everest/itp/keith/prover/prover

Modified Files:
	prove.ql trans.ql window.ql 
Log Message:
New method for storing preorder information.

Fix for trans so that it lives up to previous claims



    RCS Version:	1.11	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.10	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.9	/homes/itp/ver4/prover/prover/window.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 11:23
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	query.ql 
Log Message:
Fixed the syntax errors that resulted from an unresolved rcsmerge.


    RCS Version:	1.11	/homes/itp/ver4/prover/dbms/query.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 11:25
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	save.ql 
Log Message:
Restored support for save_clauses (used to save compiled rules).
Undid the change from writeln('.') to put(46), because Qu-Prolog is fixed.


    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/save.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 11:28
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	comprule.ql 
Log Message:
Added an ancestor check so that compiled theorems from descendent theories
do not contribute to the proof.  Also, ensured that compiled_rule/2
commands cause the theory to be saved correctly (by calling update_dir/1).


    RCS Version:	1.3	/homes/itp/ver4/prover/dbms/comprule.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 14:46
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	comprule.ql 
Log Message:
Renamed subset_chk and member_chk to more standard Prolog names.
Moved them into lib/tools.ql.


    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/comprule.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 14:46
author: marku
Update of /homes/itp/ver4/prover/lib
In directory everest:/u0/everest/marku/Ergo/prover/lib

Modified Files:
	tools.ql 
Log Message:
Renamed subset_chk and member_chk to more standard Prolog names.
Moved them into lib/tools.ql.


    RCS Version:	1.3	/homes/itp/ver4/prover/lib/tools.ql,v

**************************************
date: Wednesday, November 17, 1993 @ 15:05
author: itp
Update of /homes/itp/ver4/prover/prover
In directory everest:/u1/everest/itp/keith/prover/prover

Modified Files:
	trans.ql 
Log Message:
Bug fix for trans




    RCS Version:	1.11	/homes/itp/ver4/prover/prover/trans.ql,v

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

Modified Files:
	assert.ql comprule.ql fact_types.ql main.ql query.ql save.ql 
	syntax1.ql syntax2.ql theory_dag.ql theory_data.ql unix.ql 
	win_rule.ql 
Log Message:
Added copyright message and CVS $Id:$ line.


    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/assert.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/comprule.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/fact_types.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/main.ql,v
    RCS Version:	1.12	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/save.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/syntax1.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/syntax2.ql,v
    RCS Version:	1.11	/homes/itp/ver4/prover/dbms/theory_dag.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/theory_data.ql,v
    RCS Version:	1.9	/homes/itp/ver4/prover/dbms/unix.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/dbms/win_rule.ql,v

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

Modified Files:
	arith.ql development.ql io.ql iu.ql macros.ql release.ql 
	tools.ql unif.ql 
Log Message:
Added copyright message and CVS $Id:$ line.


    RCS Version:	1.4	/homes/itp/ver4/prover/lib/arith.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/lib/development.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/lib/io.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/lib/iu.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/lib/macros.ql,v
    RCS Version:	1.3	/homes/itp/ver4/prover/lib/release.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/lib/tools.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/lib/unif.ql,v

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

Modified Files:
	hyps.ql newvars.ql prove.ql take_thm.ql trans.ql window.ql 
Log Message:
Added copyright message and CVS $Id:$ line.


    RCS Version:	1.11	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.12	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/prover/take_thm.ql,v
    RCS Version:	1.12	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.10	/homes/itp/ver4/prover/prover/window.ql,v

**************************************
date: Thursday, November 18, 1993 @ 16:47
author: marku
Update of /homes/itp/ver4/prover/prover
In directory everest:/u0/everest/marku/Ergo/prover/prover

Modified Files:
	hyps.ql 
Log Message:
Restricted get_th_or_hyp so that it only generates conjectures
when it is passed an explicit c(_) term.


    RCS Version:	1.12	/homes/itp/ver4/prover/prover/hyps.ql,v

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

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


    RCS Version:	1.10	/homes/itp/ver4/prover/Makefile,v

**************************************
date: Friday, November 19, 1993 @ 14:59
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	query.ql 
Log Message:
More changes to stronger/2 to make stronger(rev(=), =) succeed.


    RCS Version:	1.13	/homes/itp/ver4/prover/dbms/query.ql,v

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

Modified Files:
	theory_dag.ql 
Log Message:
Changed the way in which stronger_than/2 is built so that it only
succeeds on functors that have been declared as preorders (or equivalences).


    RCS Version:	1.12	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

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

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


    RCS Version:	1.11	/homes/itp/ver4/prover/Makefile,v

**************************************
date: Friday, November 19, 1993 @ 16:00
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	theory_dag.ql 
Log Message:
More tweaks to stronger_than.  (add stronger_than(rev(P),rev(P)) for preorders)


    RCS Version:	1.13	/homes/itp/ver4/prover/dbms/theory_dag.ql,v

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

Modified Files:
	Makefile 
Log Message:

Dropped take_thm.ql



    RCS Version:	1.12	/homes/itp/ver4/prover/Makefile,v

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

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



    RCS Version:	1.14	/homes/itp/ver4/prover/dbms/query.ql,v

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

Modified Files:
	hyps.ql newvars.ql take_thm.ql trans.ql 
Log Message:
Pushed the 'is_theorem2' type search restrictions into
find_rule etc

Rewritten thawing_new_vars (again)


Added (finally) support for the implicit true hypothesis 

Re-Implemented take_theorem with h_trans




    RCS Version:	1.13	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/prover/take_thm.ql,v
    RCS Version:	1.13	/homes/itp/ver4/prover/prover/trans.ql,v

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

Modified Files:
	query.ql 
Log Message:
Bugfix in look_for_theorem



    RCS Version:	1.15	/homes/itp/ver4/prover/dbms/query.ql,v

**************************************
date: Monday, November 22, 1993 @ 17:36
author: itp
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u1/everest/itp/keith/prover/dbms

Modified Files:
	query.ql 
Log Message:
No change



    RCS Version:	1.16	/homes/itp/ver4/prover/dbms/query.ql,v

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

Modified Files:
	newvars.ql trans.ql 
Log Message:
Bugfix in nv_collect_vars





    RCS Version:	1.9	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.14	/homes/itp/ver4/prover/prover/trans.ql,v

**************************************
date: Thursday, November 25, 1993 @ 9:19
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	comprule.ql fact_types.ql 
Log Message:
Extended compiled rules to support the compiled_rulez clauses
(these are the same as compiled_rule clauses, except that they
are always executed *after* all compiled_rule clauses).
Also, allowed conditions to be discharged using theorems at compile time.


    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/comprule.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/fact_types.ql,v

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

Modified Files:
	comprule.ql 
Log Message:
Added the is_theorem discharge command in compiled rules.
Added checks to ensure that compiled_rulez clauses are always last.


    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/comprule.ql,v

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

Modified Files:
	query.ql theory_dag.ql unix.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!




    RCS Version:	1.17	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.14	/homes/itp/ver4/prover/dbms/theory_dag.ql,v
    RCS Version:	1.10	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	io.ql iu.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!




    RCS Version:	1.9	/homes/itp/ver4/prover/lib/io.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/lib/iu.ql,v

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

Modified Files:
	comprule.ql 
Log Message:
Added the is_theorem discharge option in compiled rules.


    RCS Version:	1.8	/homes/itp/ver4/prover/dbms/comprule.ql,v

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

Modified Files:
	trans.ql 
Log Message:
Changed the default direction of rules to be conditional forward.


    RCS Version:	1.15	/homes/itp/ver4/prover/prover/trans.ql,v

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

Modified Files:
	tools.ql 
Log Message:
Generalised elem/2 slightly.


    RCS Version:	1.5	/homes/itp/ver4/prover/lib/tools.ql,v

**************************************
date: Monday, December 6, 1993 @ 12:49
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	unix.ql 
Log Message:
Added a '-V' (for verbose) command line option which prints out the full
path name each time it tries to read a file.  This should make it easier
to debug incorrect installation problems.  Also changed the non-verbose
output so that file names are printed *before* they are loaded, rather
than after.
Added a '-lib Path' command line option which sets the library location
for the whole prover.  This means that path entries of the form lib(Dir)
now get expanded into Path/Dir.  This allows global.erg files to
be a little less system dependent.


    RCS Version:	1.11	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	comprule.ql query.ql 
Log Message:

Expanded compiled_rule:

	To interpret rules in directions other than 't'.

	To allow discharge of conditions with theorems themselves
	having conditions
	
	With 'cr_freeze/1', which allows freezing of a variable during
	definition of the compiled rule.

EG:
	compiled_rule(r:transeql, f, simp_int1,
		(simp_int1(((A * B) * C), _) :-
			integer(B), integer(C), cr_freeze(C),
			1=arith:mul_assoc,
			[1,1]=int(_),
			[1,2]=int(_),
			[1,3]=int(_),
			2=simp_int_subterm(A * _, A * _))).


	It may be necessary to modify existing compiled rule declarations to
	add the direction argument.



    RCS Version:	1.9	/homes/itp/ver4/prover/dbms/comprule.ql,v
    RCS Version:	1.18	/homes/itp/ver4/prover/dbms/query.ql,v

**************************************
date: Thursday, December 9, 1993 @ 14:51
author: marku
Update of /homes/itp/ver4/prover/lib
In directory everest:/u0/everest/marku/Ergo/prover/lib

Modified Files:
	tools.ql 
Log Message:
Added append/2.


    RCS Version:	1.6	/homes/itp/ver4/prover/lib/tools.ql,v

**************************************
date: Thursday, December 9, 1993 @ 14:51
author: marku
Update of /homes/itp/ver4/prover
In directory everest:/u0/everest/marku/Ergo/prover

Modified Files:
	Makefile 
Log Message:
Added some debug messages to help fix a current dir. problem with qc.


    RCS Version:	1.13	/homes/itp/ver4/prover/Makefile,v

**************************************
date: Thursday, December 9, 1993 @ 14:52
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	unix.ql 
Log Message:
Changed the help command to pass the library directory to the help script.


    RCS Version:	1.12	/homes/itp/ver4/prover/dbms/unix.ql,v

**************************************
date: Thursday, December 9, 1993 @ 15:03
author: marku
Update of /homes/itp/ver4/prover/dbms
In directory everest:/u0/everest/marku/Ergo/prover/dbms

Modified Files:
	comprule.ql 
Log Message:
Removed debug messages from eval_compiled_rule.


    RCS Version:	1.10	/homes/itp/ver4/prover/dbms/comprule.ql,v

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

Modified Files:
	Makefile 
Added Files:
	ergo.template 
Log Message:
Added ergo.template: a variant of the ergo script, which is used
during the installation process to generate the ergo script.


    RCS Version:	1.1	/homes/itp/ver4/prover/ergo.template,v
    RCS Version:	1.14	/homes/itp/ver4/prover/Makefile,v

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

Modified Files:
	comprule.ql 
Log Message:
Minor changes.


    RCS Version:	1.11	/homes/itp/ver4/prover/dbms/comprule.ql,v

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

Modified Files:
	iu.ql 
Log Message:
Restored some changes (esp. complete_retry_delays) that were lost earlier.


    RCS Version:	1.7	/homes/itp/ver4/prover/lib/iu.ql,v

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

Modified Files:
	Makefile 
Log Message:
Added the -lib Path option to the generated 'ergo' script.


    RCS Version:	1.15	/homes/itp/ver4/prover/Makefile,v

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

Modified Files:
	unix.ql 
Log Message:
Restored the -L option for preloaded files.


    RCS Version:	1.13	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	unix.ql 
Log Message:
Removed the lib(_) output from the consult messages.


    RCS Version:	1.14	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	Makefile 
Log Message:
Changed location of global.erg to be with all the other .erg
files in LIBRARY_DIRECTORY/thy.


    RCS Version:	1.16	/homes/itp/ver4/prover/Makefile,v

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

Modified Files:
	unix.ql 
Log Message:
Removed the debug message from the help command.


    RCS Version:	1.15	/homes/itp/ver4/prover/dbms/unix.ql,v

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

Modified Files:
	assert.ql comprule.ql fact_types.ql main.ql query.ql save.ql 
	syntax1.ql syntax2.ql theory_dag.ql theory_data.ql unix.ql 
	win_rule.ql 
Log Message:
Updated-Copyright

    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/assert.ql,v
    RCS Version:	1.12	/homes/itp/ver4/prover/dbms/comprule.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/dbms/fact_types.ql,v
    RCS Version:	1.6	/homes/itp/ver4/prover/dbms/main.ql,v
    RCS Version:	1.19	/homes/itp/ver4/prover/dbms/query.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/dbms/save.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/syntax1.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/syntax2.ql,v
    RCS Version:	1.15	/homes/itp/ver4/prover/dbms/theory_dag.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/dbms/theory_data.ql,v
    RCS Version:	1.16	/homes/itp/ver4/prover/dbms/unix.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/dbms/win_rule.ql,v

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

Modified Files:
	arith.ql development.ql io.ql iu.ql macros.ql release.ql 
	tools.ql unif.ql 
Log Message:
Updated-Copyright

    RCS Version:	1.5	/homes/itp/ver4/prover/lib/arith.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/lib/development.ql,v
    RCS Version:	1.10	/homes/itp/ver4/prover/lib/io.ql,v
    RCS Version:	1.8	/homes/itp/ver4/prover/lib/iu.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/lib/macros.ql,v
    RCS Version:	1.4	/homes/itp/ver4/prover/lib/release.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/lib/tools.ql,v
    RCS Version:	1.5	/homes/itp/ver4/prover/lib/unif.ql,v

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

Modified Files:
	hyps.ql newvars.ql prove.ql take_thm.ql trans.ql window.ql 
Log Message:
Updated-Copyright

    RCS Version:	1.14	/homes/itp/ver4/prover/prover/hyps.ql,v
    RCS Version:	1.10	/homes/itp/ver4/prover/prover/newvars.ql,v
    RCS Version:	1.13	/homes/itp/ver4/prover/prover/prove.ql,v
    RCS Version:	1.7	/homes/itp/ver4/prover/prover/take_thm.ql,v
    RCS Version:	1.16	/homes/itp/ver4/prover/prover/trans.ql,v
    RCS Version:	1.11	/homes/itp/ver4/prover/prover/window.ql,v

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

Modified Files:
	query.ql 
Log Message:
Another fix to equal_to/2 to ensure that it handles variable
arguments, but also simplifies rev(E) where E is an equivalence.


    RCS Version:	1.20	/homes/itp/ver4/prover/dbms/query.ql,v
