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

Added Files:
	arith.thy fol.thy fun.thy r.thy r_plus.thy 
Log Message:
Added the global .thy files (exact copies from the release4.2 directory)


    RCS Version:	1.1	/homes/itp/ver4/thy/arith.thy,v
    RCS Version:	1.1	/homes/itp/ver4/thy/fol.thy,v
    RCS Version:	1.1	/homes/itp/ver4/thy/fun.thy,v
    RCS Version:	1.1	/homes/itp/ver4/thy/r.thy,v
    RCS Version:	1.1	/homes/itp/ver4/thy/r_plus.thy,v

**************************************
date: Wednesday, October 13, 1993 @ 8:25
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Modified Files:
	arith.thy 
Log Message:
Added the 'arith_types' rule group.


    RCS Version:	1.2	/homes/itp/ver4/thy/arith.thy,v

**************************************
date: Wednesday, October 13, 1993 @ 8:38
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Added Files:
	Makefile 
Log Message:
Added a Makefile with two targets:
     thy      --- checks all the latest .thy files out of RCS.
     install  --- copies all the .thy files into ~itp/Ergo/thy.


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

**************************************
date: Monday, October 18, 1993 @ 10:43
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Modified Files:
	arith.thy r.thy 
Log Message:
Removed a redundant hypothesis from some lt_ and le_ theorems in 'arith'.
Added the rewrite.ql tactic file to the 'r' theory.


    RCS Version:	1.3	/homes/itp/ver4/thy/arith.thy,v
    RCS Version:	1.2	/homes/itp/ver4/thy/r.thy,v

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

Modified Files:
	fol.thy r.thy 
Log Message:
I didn't do nuffin!



    RCS Version:	1.2	/homes/itp/ver4/thy/fol.thy,v
    RCS Version:	1.3	/homes/itp/ver4/thy/r.thy,v

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

Modified Files:
	r_plus.thy 
Log Message:
Added the r:local_substitutivity theorem.


    RCS Version:	1.2	/homes/itp/ver4/thy/r_plus.thy,v

**************************************
date: Thursday, October 21, 1993 @ 13:01
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Modified Files:
	fun.thy 
Log Message:
Removed is_boolean, since bool/1 is defined in 'r'.


    RCS Version:	1.2	/homes/itp/ver4/thy/fun.thy,v

**************************************
date: Monday, November 1, 1993 @ 11:57
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Modified Files:
	arith.thy 
Log Message:
Fixed side condition of eval_not_eq (changed Prolog not to \+).


    RCS Version:	1.4	/homes/itp/ver4/thy/arith.thy,v

**************************************
date: Monday, November 1, 1993 @ 17:10
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Modified Files:
	Makefile 
Log Message:
Added the ergo theory to the Makefile.


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

**************************************
date: Monday, November 1, 1993 @ 17:14
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Added Files:
	ergo.thy 
Log Message:
Added ergo.thy


    RCS Version:	1.1	/homes/itp/ver4/thy/ergo.thy,v

**************************************
date: Friday, November 5, 1993 @ 12:56
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Modified Files:
	arith.thy 
Log Message:
Added the theorems and tactics for Alena Griffith's Linear Arithmetic Solver.


    RCS Version:	1.5	/homes/itp/ver4/thy/arith.thy,v

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

Modified Files:
	arith.thy 
Log Message:
Added:   abbreviation A:nats === int(A) and 0 =< A.


    RCS Version:	1.6	/homes/itp/ver4/thy/arith.thy,v

**************************************
date: Monday, November 22, 1993 @ 17:35
author: marku
Update of /homes/itp/ver4/thy
In directory everest:/u0/everest/marku/Ergo/thy

Modified Files:
	arith.thy 
Log Message:
Added an extra check to the body of the eval_eq axiom.


    RCS Version:	1.7	/homes/itp/ver4/thy/arith.thy,v

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

Modified Files:
	arith.thy 
Log Message:
Added a compiled rule for integer typing.


    RCS Version:	1.8	/homes/itp/ver4/thy/arith.thy,v

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

Modified Files:
	arith.thy 
Log Message:
Changed I:nats from an abbrevation to the real thing.
Proved the nat_induction2 rule which uses I:nats and introduces
I+1 rather than succ(I).
Did a temporary fix to the compiled rule for integer typing.


    RCS Version:	1.9	/homes/itp/ver4/thy/arith.thy,v

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

Modified Files:
	ergo.thy 
Log Message:
Changed the theorem commands to rerun commands.


    RCS Version:	1.2	/homes/itp/ver4/thy/ergo.thy,v
