#
c4dc578b |
|
17-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Fix up proofs after word lemma moves
|
#
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.
|
#
4f68967b |
|
28-Aug-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2017: update AInvs for RC0 * word_eqI is no longer rule_format. * Updated Isabelle/ML Thm.join_proofs to Thm.consolidate. * Updated suffix_refl to suffix_order.order.refl. * Removed some lines of proofs, thanks to improved simplifier.
|
#
cd8a45c2 |
|
06-Apr-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm-hyp ainvs: update lookupPtSlot
|
#
331cb520 |
|
19-Feb-2017 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm-hyp: AInvs down to detype
|
#
7e79b1b7 |
|
17-Jan-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
changes after rebasing (for isabelle2016-1 and the new wp)
|
#
5cabf382 |
|
18-Dec-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: fix arch_splitting/locales * tcb_arch_ref: definition and invariants (to access obj_refs in tcb_arch in generic contexts) * fixes related hyp_refs
|
#
61dffdb6 |
|
26-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: changes from rebase for ARM_HYP invariants
|
#
1d4b6e93 |
|
26-Aug-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: updates for vcpu, alignments, valid_vspace_obj, wellformed_arch_obj, etc.
|
#
0d4e4bd2 |
|
23-Nov-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: copy arch-splitted invariant files from ARM earlier updates in ArchInvariants are kept
|
#
f0da7d17 |
|
06-Dec-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: add ARM_HYP directory, updating ArchInvariants_AI and Invariants_AI
|