History log of /seL4-l4v-10.1.1/HOL4/src/integer/jrhCore.sml
Revision Date Author Comments
# e71025ec 11-Sep-2008 Michael Norrish <Michael.Norrish@nicta.com.au>

Everywhere remove use of temp_set_grammars idiom for setting up the
local grammars, preferring instead to statically bind the appropriate
names. You need to grab Parse.Term and Parse.Type as well as Term and
Type, requiring the definition of a Parse structure.


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


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