adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/lib
History
Achim D. Brucker e59d6ad091 Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
..
Basics Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
CorresK lib+refine: rename Corres_Method to CorresK_Method 2023-06-30 10:56:47 +10:00
EVTutorial lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Eisbach_Tools lib: provide warning suppression for Eisbach methods 2024-01-15 11:08:27 +11:00
Hoare_Sep_Tactics lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
ML_Utils lib: README.md files for the new sessions 2023-01-25 11:49:59 +11:00
Monads lib: add no_ofail_if 2024-01-15 18:08:12 +10:30
Word_Lib_l4v Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
clib clib: suppress simp warnings in simpl_rewrite 2024-01-15 11:08:27 +11:00
concurrency lib/monads: improve style of nondet and trace 2023-10-05 22:00:55 +11:00
doc licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
sep_algebra Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
test lib: add docs and test for Corres_Method 2023-08-30 21:59:37 +02:00
AddUpdSimps.thy lib AddUpdSimps: cleanup + remove old debugging code 2020-05-04 17:02:58 +08:00
BCorres_UL.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Bisim_UL.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
CorresK_Method.thy lib: add new corres method 2023-06-30 15:56:42 +10:00
Corres_Adjust_Preconds.thy lib+proofs+sys-init+tools: proof updates for Fun_Pred_Syntax 2023-01-09 14:54:11 +11:00
Corres_Cases.thy lib+refine: rename Corres_Method to CorresK_Method 2023-06-30 10:56:47 +10:00
Corres_Method.thy lib: factor out is_safe_wp method 2023-08-30 21:59:37 +02:00
Corres_UL.thy lib: add corres_if_strong 2024-01-15 18:08:12 +10:30
Crunch.ML lib: add warnings to crunch_ignore 2022-05-27 15:03:10 +10:00
Crunch.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
Crunch_Instances_NonDet.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Crunch_Instances_Trace.thy lib: update for trace monad refactor 2023-08-23 11:53:22 +10:00
CutMon.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
DataMap.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Defs.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
DetWPLib.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Distinct_Cmd.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
EquivValid.thy lib+proof: proof updates for wpc change 2023-06-15 09:52:15 +10:00
Eval_Bool.thy isabelle2021-1 lib: update Lib session, retire wpx 2022-03-29 08:38:25 +11:00
ExtraCorres.thy lib: add ifM_corres' and orM_corres' 2024-01-15 18:08:12 +10:30
Extract_Conjunct.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
FP_Eval.thy lib: always prefer Main to HOL.HOL import 2023-01-25 11:48:38 +11:00
FastMap.thy isabelle2021-1 lib: update Lib session, retire wpx 2022-03-29 08:38:25 +11:00
Find_Names.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
GenericLib.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
GenericTag.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Guess_ExI.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
HaskellLemmaBucket.thy lib: introduce [empty_fail] and merge EmptyFailLib 2023-02-09 11:46:50 +11:00
HaskellLib_H.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Heap_List.thy lib: some sym_heap lemmas regarding heap updates 2024-01-15 18:08:12 +10:30
Injection_Handler.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Insulin.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
LemmaBucket.thy lib+aarch64 refine: move lemmas to lib 2023-09-27 14:28:36 +10:00
LexordList.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
Lib.thy Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
ListLibLemmas.thy lib: add defn of list_insert_before, and some lemmas 2024-01-15 18:08:12 +10:30
List_Lib.thy lib: add defn of list_insert_before, and some lemmas 2024-01-15 18:08:12 +10:30
Locale_Abbrev.thy isabelle-2021: Lib update 2021-09-30 16:53:17 +10:00
ML_Goal.thy lib: Isabelle2023 update 2023-10-06 14:29:15 +11:00
ML_Goal_Test.thy lib+tools: MLUtils -> ML_Utils for consistency 2023-01-20 13:43:39 +11:00
Match_Abbreviation.thy cleanup: reduce warnings 2021-09-30 16:53:17 +10:00
Monad_Commute.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Monad_Lists.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
MonadicRewrite.thy lib: add monadic_rewrite_corres_r_generic_ex_abs 2024-01-15 18:08:12 +10:30
More_Numeral_Type.thy Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
NICTATools.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
Named_Eta.thy lib: add named_eta and no_name_eta methods 2022-09-06 02:50:23 +10:00
NonDetMonadLemmaBucket.thy Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
Oblivious.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Qualify.thy lib: Isabelle2023 update 2023-10-06 14:29:15 +11:00
ROOT Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
RangeMap.thy lib: make ML_Utils a separate session 2023-01-20 13:43:39 +11:00
Repeat_Attribute.thy lib: add attribute to repeatedly apply other attributes 2020-11-09 17:18:41 +11:00
Requalify.thy lib: Isabelle2023 update 2023-10-06 14:29:15 +11:00
Rules_Tac.thy lib: add rules_tac and related multi-thm instantiators 2022-09-10 06:29:19 +10:00
ShowTypes.thy cleanup: reduce warnings 2021-09-30 16:53:17 +10:00
SimpStrategy.thy isabelle2021-1 lib: update Lib session, retire wpx 2022-03-29 08:38:25 +11:00
Simulation.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Solves_Tac.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
SpecValid_R.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
SplitRule.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
StateMonad.thy lib: factor out and generalise bool syntax for functions 2023-01-09 14:54:06 +11:00
SubMonadLib.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Time_Methods_Cmd.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Try_Attribute.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Try_Methods.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
Value_Abbreviation.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Value_Type.thy lib: avoid @{file} for files that might be moved 2022-10-31 11:45:05 +11:00
crunch-cmd.ML lib+proofs+sys-init+tools: proof updates for Fun_Pred_Syntax 2023-01-09 14:54:11 +11:00
defs.ML lib: Isabelle2023 update 2023-10-06 14:29:15 +11:00
set.ML licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
tests.xml lib: A tutorial and some 'modify' monad rules for Lib.EquivValid 2020-11-17 06:06:03 +11:00