#
eee03790 |
|
05-Mar-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make equality of "tight" precedence by default Start to work through knock-on effects of this.
|
#
9420ca26 |
|
10-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Moved hol-light's wellorder theorems into HOL4's wellorderTheory
|
#
6a81a039 |
|
21-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from src Will also make selftest to check that they aren't introduced
|
#
95d60bd3 |
|
02-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove -- as an alias for Term parser. As per comment in release notes this has long been replaced as appropriate style.
|
#
94b064b9 |
|
15-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove unnecessary structure bracketting As per 89fc99bc3, but on as many examples as a grep -R can find.
|
#
bd77b8fb |
|
20-Oct-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace
|
#
58cc1c29 |
|
04-Oct-2015 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
using new lemmas to prove existing theorems easier
|
#
1cadbb4e |
|
04-Oct-2015 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
using LESS_ALT to prove WF_LESS more easily
|
#
a8a882f5 |
|
04-Oct-2015 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
use of LESS_ALT to give shorter proofs
|
#
f570e462 |
|
04-Oct-2015 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
LESS_ALT, alternative definition of <
|
#
764cbf59 |
|
04-Oct-2015 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
inverse of LESS_MONO
|
#
6dacfbcf |
|
04-Oct-2015 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
shorter proof of LESS_MONO requires moving definition of PRE forward
|
#
c14b5cc3 |
|
04-Oct-2015 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
new proof of LESS_0 uses existing proof of LESS_0_0, doesn't require LESS_THM
|
#
ceff34b8 |
|
10-Apr-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Make a couple of important termination theorems automatic rewrites. In particular: |- WF $< |- inv_image R f x y <=> R (f x) (f y)
|
#
47f146b5 |
|
23-Nov-2012 |
Ramana Kumar <ramana.kumar@gmail.com> |
add some more OpenTheory names to the map
|
#
f8fd8324 |
|
02-Oct-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
add various names to the OpenTheory map This is in preparation for logging llistTheory. Notes: - Sent combin$C to Function.Combinator.c (same for combin$S). Another name might be preferred on the OpenTheory side. - Not sure what bool$BOUNDED is about; dumped it in the HOL4 namespace. - Put lots of pred_set constants in the Set namespace, but in the standard (OpenTheory) library it seems like Set is for constants operating on an abstract type of sets (rather than predicates). I'm not sure whether we should use a different namespace when working with sets-as-predicates or just pretend predicates are the abstract type and do a bit of magic on article reading/writing as necessary (don't know what that would be exactly yet). - Similar for constants in set_relation, which I'm currently putting in the Relation namespace. Although it looks like currently OpenTheory doesn't use an abstract type of relations (but probably it will later). - Sent marker$Cong and marker$Abbrev to Unwanted.id, but not sure if Unwanted.id is supposed to be polymorphic (whereas those are identity functions restricted to bool). Similar for numeral$iZ - sent GSPEC to Set.specification; maybe not an obvious name... - Using top-level "While" namespace for whileTheory - dumped numeral$iiSUC in HOL4 namespace; not sure what to do with it - BIT2 is going to Number.Numeral.bit2; this is in line with wanting the base library to be liberal, i.e. a union of all useful basic constants and theorems (so has bit0, bit1 and bit2)... but I think there may be competing goals for base
|
#
930481be |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make a couple of theorems about prim_rec$measure automatic rewrites.
|
#
3e12521d |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete unnecessary infix declarations in prim_recScript.sml.
|
#
9729734b |
|
22-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Attempt to tidy-up HOL's output in non-interactive mode - mostly through lining up definition and theorem names.
|
#
38ed962b |
|
19-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
TeX macros in TeX_notation calls need to be terminated with {}.
|
#
621bb980 |
|
17-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move more TeX notations into appropriate theory files. Word-related notation still to do.
|
#
d9003833 |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fairly dramatic change, supporting the use of "syntactic patterns". It is now possible to overload a name to term (typically a lambda-abstraction) in order to create syntax-only definitions. For example, there is a definition of not-equals now in the system: val _ = overload_on ("<>", ``\x y. ~(x = y)``) val _ = set_fixity "<>" (Infix(NONASSOC, 450)) This definition is parsed and pretty-printed. Two other annoying changes. The interface for adding unicode variants has changed, and I have made precedence level 450 of the parser non-associative. This latter change has caused most of the (minor) adjustments to the files below. The regression test doesn't go through yet. (Currently there is a failure in quotient/examples/sigma that I don't understand.)
|
#
f33e0630 |
|
05-Mar-2007 |
Joe Hurd <joe@gilith.com> |
Did some community service expunging all occurrences of the old syntax for if-then-else from the HOL distribution. Apologies if I've broken your example or development: you can either upgrade it to use the new syntax or else issue the magic parser incantation that I chopped out of boolScript.sml on this check in.
|
#
d6b08f6b |
|
16-Aug-2002 |
Konrad Slind <konrad.slind@gmail.com> |
Change to type of new_specification, and made it tell that parser about the introduced constants. Lots of knock-on (trivial) mods.
|
#
4ac64eb2 |
|
22-Feb-2002 |
Konrad Slind <konrad.slind@gmail.com> |
Various bits of messing about.
|
#
0f93948d |
|
16-Nov-2000 |
Konrad Slind <konrad.slind@gmail.com> |
paired syntax.
|
#
2bcd4eee |
|
07-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes making directory Kananaskis compatible.
|
#
ba27d3d8 |
|
20-Jul-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Further simplifications of number theory to remove dependence on axiom of choice.
|
#
b6a894e1 |
|
10-Dec-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes due to the incorporation of John Harrison's datatype definition package.
|
#
88242741 |
|
02-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Change to structure of numLib so that reduce and arith are incorporated.
|