#
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.
|