#
a45adef6 |
|
31-Oct-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
all: remove theory import path references In Isabelle2020, when isabelle jedit is started without a session context, e.g. `isabelle jedit -l ASpec`, theory imports with path references cause the isabelle process to hang. Since sessions now declare directories, Isabelle can find those files without path reference and we therefore remove all such path references from import statements. With this, `jedit` and `build` should work with and without explicit session context as before. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
408bf413 |
|
19-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: Isabelle2020 update 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
|
#
327bed74 |
|
12-Dec-2019 |
Rafal Kolanski <rafal.kolanski@data61.csiro.au> |
lib: migrate distinct_map_enum into Lib
|
#
44bdf90a |
|
18-Jul-2019 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
autocorres, lib: refactor `nat :: bit_operations` instance This refactors the instances in HaskellLib and AutoCorres into a new theory, Lib.NatBitwise.
|
#
c34840d0 |
|
05-Jun-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
global: isabelle update_cartouches
|
#
6ff1a38f |
|
23-May-2019 |
Michael McInerney <Michael.McInerney@data61.csiro.au> |
lib: update for Isabelle 2019
|
#
f2613b28 |
|
17-Oct-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: additional setup for numeral types In particular: instantiate to the size class so one can use bounded types for automatic termination measures in fun.
|
#
0044c57e |
|
26-Aug-2018 |
Ilya Yanok <ilya.yanok@gmail.com> |
lib: change runErrorT to runExceptT to match Haskell code
|
#
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>")
|
#
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.
|
#
53fde5e5 |
|
29-Jul-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib/design: enable more Haskell-like list comprehension syntax Accept "[f x | x \leftarrow t]" in addition to "[f x . x \leftarrow t]", because the former is what naturally comes out of the Haskell translator, and the regexps that would be necessary in the Haskell translator for this are distasteful. JIRA-VER 927
|
#
24fbac1e |
|
29-Jul-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: remove non-exhaustive pattern warning
|
#
d4996217 |
|
13-Jun-2018 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
lib: add generic lemmas from SELFOUR-584 updates Mainly concerning word_ctz and enumeration_both.
|
#
e99bd4d5 |
|
20-Mar-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
lib: properly defining arrayListUpdate (Fix)
|
#
6ed990f1 |
|
05-Sep-2016 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
VER-520: Change (>>) for (>>_) This is a know issue that was naively solved using `infixl ">>_"` which effectively does nothing since "_" has an special meaning. `infixl ">>'_"` was introduced to fix the issue. has a special meaning tags: [VER-520]
|
#
cc8d10a2 |
|
19-May-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
lib: arch-splitted WordSetup, fixed lib theory includes
|
#
f88c4184 |
|
13-May-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib: move Distinct_Prop out of Word_Lib
|
#
f0faa90f |
|
17-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib/spec/proof/tools: fix word change fallout
|
#
84b923a6 |
|
17-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib: start disentangling spaghetti word dependencies
|
#
0126ea53 |
|
27-Apr-2016 |
agomezl <alegomez544@gmail.com> |
Change (>>) by (>>_)
|
#
b7563eb7 |
|
11-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
fix lib for isabelle 2016
|
#
e4d8fb5d |
|
24-Nov-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
GHC 7.8 update (bitSize -> finiteBitSize)
|
#
12b1b0d1 |
|
08-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
move isAligned to HaskellLib Isabelle2014 doesn't like defs to be less general than the consts declaration.
|
#
1af1d2b6 |
|
08-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
some of the global Isabelle2014 renames option_case -> case_option sum_case -> case_sum prod_case -> case_prod Option.set -> set_option Option.map -> map_option option_rel -> rel_option list_all2_def -> list_all2_iff map.simps -> list.map tl.simps -> list.sel(2-3) the.simps -> option.sel
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|