History log of /seL4-l4v-10.1.1/HOL4/src/integer/CooperCore.sml
Revision Date Author Comments
# d2c33299 05-Nov-2014 Michael Norrish <michael.norrish@nicta.com.au>

Remove some Unicode in src/


# 9d250cb1 22-Oct-2012 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix bug in Cooper's algorithm; build-sequence at selftest=0 builds.

Progress with #52.


# a78bc2d4 21-Oct-2012 Michael Norrish <michael.norrish@nicta.com.au>

Attempt to fix cooper_conv bug.

COOPER_CONV ``~(&a + &b < 0)`` still fails.


# 412ba3f7 12-Aug-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Commented out some profiling code.


# cf44c939 11-Sep-2008 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix for a bug found by Mike. Problem was the use of a theorem's
choice of bound name, which caused a clash with a user's free name.
Genvar to the rescue.


# ff453f9e 11-Sep-2008 Michael Norrish <Michael.Norrish@nicta.com.au>

Add an embodiment of the Omega d.p. for use inside the simplifier. It
can perform quite badly on goals with too many disjunctive assumptions
(and ~(x = y) counts as a disjunction).


# 547d9123 17-Apr-2008 Scott Owens <Scott.Owens@cl.cam.ac.uk>

Remove character number 160 from a comment


# 007e43f2 31-May-2005 Konrad Slind <konrad.slind@gmail.com>

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml


# b5d074e2 22-Aug-2002 Michael Norrish <Michael.Norrish@nicta.com.au>

Upgraded references to UNBETA_CONV and mk_abs_CONV (both essentially the
same function) and removed implementations because of provision of this
function in Conv.


# f84f60b3 12-Oct-2001 Konrad Slind <konrad.slind@gmail.com>

30 lashes with a wet noodle to mn200! Forgetting to put
structure foo = struct ... end
around some files causes very odd error messages from mosmlc on Windows.


# 4ae3e9df 14-Sep-2001 Michael Norrish <Michael.Norrish@nicta.com.au>

More reorganisation, mainly to remove listTheory as an ancestory wherever
possible (it still persists as a necessary ancestor of CooperCore, but
isn't used un-necessarily elsewhere).
Also sped up phase5 of CooperCore some more.


# 99abe76d 13-Sep-2001 Michael Norrish <Michael.Norrish@nicta.com.au>

Total reorganisation of Cooper code. Two ..Core modules can be swapped
in and out of CooperShell to provide "shadow syntax" or my original
implementation of the core phases of the algorithm. Code currently littered
with profiler guff.