Commit Graph

14 Commits

Author SHA1 Message Date
Gerwin Klein 24fbac1e67 lib: remove non-exhaustive pattern warning 2018-08-06 11:22:53 +10:00
Rafal Kolanski d4996217b3 lib: add generic lemmas from SELFOUR-584 updates
Mainly concerning word_ctz and enumeration_both.
2018-06-15 18:48:47 +10:00
Alejandro Gomez-Londono e99bd4d5f2 lib: properly defining arrayListUpdate (Fix) 2017-06-19 14:32:27 +10:00
Alejandro Gomez-Londono 6ed990f1da 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]
2016-09-05 16:56:13 +10:00
Joel Beeren cc8d10a217 lib: arch-splitted WordSetup, fixed lib theory includes 2016-05-20 12:26:04 +10:00
Gerwin Klein f88c4184ff lib: move Distinct_Prop out of Word_Lib 2016-05-16 21:11:40 +10:00
Gerwin Klein f0faa90f8a lib/spec/proof/tools: fix word change fallout 2016-05-16 21:11:40 +10:00
Gerwin Klein 84b923a677 lib: start disentangling spaghetti word dependencies 2016-05-16 21:11:40 +10:00
agomezl 0126ea53f8 Change (>>) by (>>_) 2016-04-27 16:08:02 +10:00
Daniel Matichuk b7563eb788 fix lib for isabelle 2016 2016-01-12 14:58:16 +11:00
Gerwin Klein e4d8fb5dba GHC 7.8 update (bitSize -> finiteBitSize) 2014-11-28 08:58:57 +11:00
Gerwin Klein 12b1b0d16f move isAligned to HaskellLib
Isabelle2014 doesn't like defs to be less general than the consts declaration.
2014-08-09 15:59:24 +10:00
Gerwin Klein 1af1d2b67b 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
2014-08-09 15:39:20 +10:00
Gerwin Klein 2a03e81df4 Import release snapshot. 2014-07-14 21:32:44 +02:00