#
b5cdf470 |
|
13-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
globally use session-qualified imports; add Lib session Session-qualified imports will be required for Isabelle2018 and help clarify the structure of sessions in the build tree. This commit mainly adds a new set of sessions for lib/, including a Lib session that includes most theories in lib/ and a few separate sessions for parts that have dependencies beyond CParser or are separate AFP sessions. The group "lib" collects all lib/ sessions. As a consequence, other theories should use lib/ theories by session name, not by path, which in turns means spec and proof sessions should also refer to each other by session name, not path, to avoid duplicate theory errors in theory merges later.
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
e2ad6f76 |
|
28-Mar-2017 |
Daniel Matichuk <daniel.matichuk@data61.csiro.au> |
lib/rule_by_method: add "atomized" attribute This recovers the original behaviour of the "atomize" attribute, which converts a Pure rule into a HOL one.
|
#
f49fa48a |
|
20-Mar-2017 |
Daniel Matichuk <daniel.matichuk@data61.csiro.au> |
rule-by-method: more robust handling of dummy thms More struggling due to no proper check for whether or not a closure is being formed
|
#
f9377219 |
|
19-Mar-2017 |
Daniel Matichuk <daniel.matichuk@data61.csiro.au> |
rule_by_method: better support for method closures We short-circuit the passed method if it looks like we're making a closure, instead just emitting a dummy "free" theorem.
|
#
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.
|
#
86bd63e4 |
|
24-Nov-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: work around a find_theorems incompatibility The new find_theorems tries to inspect rule_prems, which previously raised an exception within Rule_By_Method. This just makes rule_prems an empty dynamic fact.
|
#
f0faa90f |
|
17-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib/spec/proof/tools: fix word change fallout
|
#
b214ac03 |
|
17-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
resurrected "defs" command for Isabelle2016-RC1
|
#
b7563eb7 |
|
11-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
fix lib for isabelle 2016
|
#
8079c795 |
|
09-Jan-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
partial progres in Rule_By_Method
|
#
ec51ebde |
|
18-Sep-2015 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
addressed issue with meta-quantifiers JIRA VER-458
|
#
143073d5 |
|
18-Sep-2015 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
addressed issue with meta-quantifiers JIRA VER-458
|
#
b2d3cd6e |
|
07-Jul-2015 |
Daniel Matichuk <daniel.matichuk@.nicta.com.au> |
Added Rule_By_Method (@ and # attributes)
|