Hi Brian,
On 20.03.2014 15:24, Brian Huffman wrote:
I've noticed that recent changesets (up to 00112abe9b25) on testboard
have completed Pure and HOL tests, but the HOL_makeall results never
show up. (The most recent HOL_makeall report is 3253aaf73a01, dated
March 18.)
Does anyone know why
On Tue, 11 Feb 2014, Clemens Ballarin wrote:
For the processing of locale expression, facts are not really required.
Having all information related to syntax should be sufficient. I cannot
tell, though, whether facts may contain syntax in disguise of certain
attributes.
In principle there
On Fri, 28 Feb 2014, Christian Sternagel wrote:
Dear Lars,
today I first tried using the new simplifier tracing facility (within
Isabelle/jEdit). I just started but have already some questions ;)
I am still delayed elsewhere, but before we enter the hot phase of the
summer release, we
On 21 March, 2014 17:26 CET, Makarius makar...@sketis.net wrote:
On Tue, 11 Feb 2014, Clemens Ballarin wrote:
For the processing of locale expression, facts are not really required.
Having all information related to syntax should be sufficient. I cannot
tell, though, whether facts
* Basic constants of Pure use more conventional names and are always
qualified. Rare INCOMPATIBILITY, but with potentially serious
consequences, notably for tools in Isabelle/ML. The following
renaming needs to be applied:
== ~ Pure.eq
==~ Pure.imp
all
