#
77067c24 |
|
04-May-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib AddUpdSimps: cleanup + remove old debugging code The command produced warnings as debug output. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
3aa849da |
|
04-May-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: remove infix warning The (=) syntax is Isabelle, not ML, and was updated accidentally. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
6ff1a38f |
|
23-May-2019 |
Michael McInerney <Michael.McInerney@data61.csiro.au> |
lib: update for Isabelle 2019
|
#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
30122b5d |
|
10-Nov-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update to new ML API Update references to renamed ML constants; supply default arguments to functions with additional parameters; etc.
|
#
b4307091 |
|
23-Sep-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
AddUpdSimps: An addition to Lib. This is a work-in-progress tool for producing simp rules for functions on a record that don't look at all the record's state. For instance, given a record with fields a, b, c, and a function "f x = a x + b x", the tool should automatically prove that "f (c_update f x) = f x".
|