#
225dd739 |
|
31-Oct-2006 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Added documentation for the temporal_deep example
|
#
1ceea7b2 |
|
10-Oct-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Document the new words theory, and the 'a itself type. (Also move all </pre> tags to the beginning of the lines they occur on; this makes a visible difference on the layout, at least within Firefox.)
|
#
4af32660 |
|
10-Oct-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
HolBddLib makes a more sophisticated use of tags than I catered for with the API change, so I've had to add a new function to Thm called add_tag (which does the obvious). The implementation of PrimitiveBddRules changes slightly, but its API remains the same.
|
#
2b19fe85 |
|
10-Oct-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update the type of mk_oracle_thm so that it takes a string rather than a tag as first argument. This is to prevent the following scenario: - show_tags := true; > val it = () : unit - val ax = new_axiom ("foo", ``T``); > val ax = [oracles: ] [axioms: foo] [] |- T : thm - val th = mk_oracle_thm (Thm.tag ax) ([], ``F``); > val th = [oracles: ] [axioms: foo] [] |- F : thm
|
#
ed001e6a |
|
21-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add notes for new type abbreviation printing feature. Slightly adjust other entries (thanks for these, Peter and Mike) to make HTML validate.
|
#
ca8e7528 |
|
20-Sep-2006 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in release notes for XEmacs support and for literals in case expressions. Modified Files: kananaskis-4.release.html ----------------------------------------------------------------------
|
#
5cd44e7f |
|
21-Sep-2006 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Added acl2 example. Thought I'd checked this in a few days ago, but checkin must have failed, so trying again.
|
#
b458dfe5 |
|
12-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change to the inductive relations definition code to support a global, and updated "monoset", which can be updated as theories load, thereby invisibly increasing the capabilities of Hol_reln. Also simplify the implementation of derive_strong_induction, and move the entrypoint to IndDefLib. New test in src/IndDef/selftest.sml wouldn't have passed before (I believe). It is more onerous than Peter's original monoset example, which didn't feature recursion under the EVERY operator. Documented in Description and release notes. Still to update theories with appropriate calls to export_mono. (export_mono and export_rewrites are now part of bossLib's interface.)
|
#
299a0a1c |
|
24-Aug-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update discussion of caret-escapes to reflect fact that ``s1 ^ s2`` is now legitimate.
|
#
63427e28 |
|
09-Aug-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix and document bug found by Mike relating to string_EQ_CONV failing. Fix is to use fromHOLstring rather than dest_string to check if terms are string literals.
|
#
55103042 |
|
03-Aug-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Minor clean-ups in release document, and addition of paragraphs on new features in handling of quotations and string literals. If you have a example that you want mentioned in the release notes, please edit this file and put it in!
|
#
77d5bb1f |
|
13-Mar-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix a problem identified by Tom Ridge with the --rebuild_deps flag to Holmake. Now the behaviour of this flag is to just call Holmake cleanDeps before proceeding with the rest of its build.
|
#
d336902d |
|
16-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Updates brought on by the change to the behaviour of ARITH_ss etc.
|
#
5a99d0e0 |
|
15-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update documentation to reflect Konrad's TypeBase changes.
|
#
13f030c2 |
|
07-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Wide-ranging change to make the TypeBase export an interface forcing users to be concerned about which theory their types are from. Interactive users of the "induction_of", "axiom_of" and similar functions are thrown the only bone: they can effectively omit the theory parameter by using "" instead of a theory name. Prompted by a bug found by Tom Ridge where it was impossible to define a pattern matching function on a type with the same name as another type because the pattern-matching code was using dest_type and TypeBase.read on just the type-operator name.
|
#
e93d7856 |
|
05-Dec-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement and document a new, unambiguous set comprehension syntax. Only fixes required are to ieeeScript where old style =>-| if-then-else syntax was nested to extraordinary degree without any parentheses. Adding parentheses was the only thing required to fix the problem.
|
#
99a67bdd |
|
03-Nov-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Document change to std_ss.
|
#
09c0951e |
|
31-Oct-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Document latest bug fixes.
|
#
528d0ccd |
|
10-Oct-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Document EXISTS bug, and put a regression test into src/q to stop it recurring.
|
#
762d2c05 |
|
03-Oct-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Our first bug (and fix).
|