.. |
ARM
|
x64 cspec: arch-split Substitute; add sign_extend for bfgen
|
2017-06-29 17:13:18 +10:00 |
ARM_HYP
|
arm-hyp (abstract/design/machine): add ARM_HYP directories
|
2017-06-17 16:26:11 +10:00 |
Hoare_Sep_Tactics
|
Initial proof updates for combinator changes.
|
2018-03-16 14:53:22 +11:00 |
Monad_WP
|
lib: fundef termination rule for unlessE .. $ throwError ,,
|
2018-06-27 10:06:48 +02:00 |
RISCV64
|
riscv: setup cspec build for L4V_ARCH=RISCV64
|
2018-06-27 10:05:44 +02:00 |
Word_Lib
|
lib: add generic lemmas from SELFOUR-584 updates
|
2018-06-15 18:48:47 +10:00 |
X64
|
x64 cspec: arch-split Substitute; add sign_extend for bfgen
|
2017-06-29 17:13:18 +10:00 |
clib
|
clib: use proper context under FOCUS_PREMS
|
2018-03-26 14:37:22 +11:00 |
concurrency
|
lib: two examples of concurrency reasoning.
|
2018-05-28 16:53:01 +10:00 |
doc
|
Import release snapshot.
|
2014-07-14 21:32:44 +02:00 |
ml-helpers
|
Isabelle2016-1: update to new ML API
|
2017-01-05 14:26:14 +11:00 |
sep_algebra
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
subgoal_focus
|
license-tool: missing license headers + .licenseignore [VER-551]
|
2016-07-14 16:34:31 +10:00 |
AddUpdSimps.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
AdjustSchematic.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Apply_Debug.thy
|
lib/apply_debug: show protected subgoals
|
2017-04-06 12:11:54 +10:00 |
Apply_Debug_Test.thy
|
apply_debug: fix example in tutorial
|
2017-02-15 15:00:23 +11:00 |
Apply_Trace.thy
|
Isabelle2017: update lib for RC0
|
2017-10-30 12:23:26 +11:00 |
Apply_Trace_Cmd.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
AutoLevity.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
AutoLevity_Base.thy
|
Isabelle2017: update lib for RC0
|
2017-10-30 12:23:26 +11:00 |
AutoLevity_Hooks.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
AutoLevity_Run.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
AutoLevity_Test.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
AutoLevity_Theory_Report.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
BCorres_UL.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Bisim_UL.thy
|
Initial proof updates for combinator changes.
|
2018-03-16 14:53:22 +11:00 |
BitFieldProofsLib.thy
|
lib: faster simplification for common cases of word_and_max_word
|
2017-12-21 21:41:01 +11:00 |
CTranslationNICTA.thy
|
lib/spec/proof/tools: fix word change fallout
|
2016-05-16 21:11:40 +10:00 |
Conjuncts.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
CorresK_Lemmas.thy
|
lib/corres_method: more corresK map rules
|
2017-07-18 12:13:16 -06:00 |
Corres_Adjust_Preconds.thy
|
Add some comments.
|
2017-08-04 11:28:54 +10:00 |
Corres_Method.thy
|
lib/wp: Remove old wp combinator rules.
|
2018-03-16 14:51:31 +11:00 |
Corres_Test.thy
|
lib/corres_method: tuning and documentation
|
2017-07-17 13:09:46 -06:00 |
Corres_UL.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch.ML
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch_Instances_NonDet.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch_Instances_Trace.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch_Test_NonDet.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch_Test_Qualified_NonDet.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch_Test_Qualified_Trace.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
Crunch_Test_Trace.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
DataMap.thy
|
SELFOUR-444: Adjust Haskell, new ghost data.
|
2016-11-02 11:19:09 +11:00 |
Defs.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Distinct_Cmd.thy
|
Isabelle2016-1: update to new ML API
|
2017-01-05 14:26:14 +11:00 |
Distinct_Prop.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Eisbach_Methods.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
EmptyFailLib.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
EquivValid.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Eval_Bool.thy
|
Expand eval_bool; add a method word_eqI_solve.
|
2017-11-01 17:30:46 +11:00 |
ExpandAll.thy
|
lib/spec/proof/tools: fix word change fallout
|
2016-05-16 21:11:40 +10:00 |
Extend_Locale.thy
|
Isabelle2017: update lib for RC0
|
2017-10-30 12:23:26 +11:00 |
ExtraCorres.thy
|
lib/wp: Remove old wp combinator rules.
|
2018-03-16 14:51:31 +11:00 |
Extract_Conjunct.thy
|
lib: add methods for extracting conjuncts from the conclusion
|
2017-11-28 19:02:49 +11:00 |
Find_Names.thy
|
lib: add find_names command to find other names of a theorem
|
2018-02-25 21:47:35 +11:00 |
GenericLib.thy
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
GenericLib_C.thy
|
Import release snapshot.
|
2014-07-14 21:32:44 +02:00 |
HaskellLemmaBucket.thy
|
Expand eval_bool; add a method word_eqI_solve.
|
2017-11-01 17:30:46 +11:00 |
HaskellLib_H.thy
|
lib: add generic lemmas from SELFOUR-584 updates
|
2018-06-15 18:48:47 +10:00 |
Insulin.thy
|
Isabelle2016-1: update to new ML API
|
2017-01-05 14:26:14 +11:00 |
LemmaBucket.thy
|
lib: add generic lemmas from SELFOUR-584 updates
|
2018-06-15 18:48:47 +10:00 |
LemmaBucket_C.thy
|
x64: merge master
|
2017-07-21 11:27:12 +10:00 |
LexordList.thy
|
lib: add theory LexordList, for lexicographical string comparison
|
2018-05-21 14:22:54 +10:00 |
Lib.thy
|
lib: some simple rules about rtrancl/rtranclp.
|
2018-05-28 15:39:39 +10:00 |
ListLibLemmas.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
List_Lib.thy
|
Lib: Addition of auxiliary lemmas in basic theories to better support CRefine
|
2016-11-25 13:05:56 +11:00 |
Match_Abbreviation.thy
|
lib: Replace subseq->match abbreviation.
|
2018-05-10 15:00:22 +10:00 |
Match_Abbreviation_Test.thy
|
lib: Replace subseq->match abbreviation.
|
2018-05-10 15:00:22 +10:00 |
MonadEq.thy
|
lib: start disentangling spaghetti word dependencies
|
2016-05-16 21:11:40 +10:00 |
MonadicRewrite.thy
|
lib: add generic lemmas from SELFOUR-584 updates
|
2018-06-15 18:48:47 +10:00 |
NICTATools.thy
|
lib: add time_methods method for comparing proof tactic speeds
|
2018-05-21 14:30:00 +10:00 |
NonDetMonadLemmaBucket.thy
|
lib/wp: Standard when/unless/whenE/unlessE rules.
|
2018-03-16 14:56:11 +11:00 |
ProvePart.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Qualify.thy
|
Isabelle2017: update lib for RC0
|
2017-10-30 12:23:26 +11:00 |
Requalify.thy
|
Isabelle2017: update lib for RC0
|
2017-10-30 12:23:26 +11:00 |
Rule_By_Method.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
SIMPL_Lemmas.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
ShowTypes.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
SimpStrategy.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
SimplRewrite.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Simulation.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Solves_Tac.thy
|
license-tool: missing license headers + .licenseignore [VER-551]
|
2016-07-14 16:34:31 +10:00 |
SpecValid_R.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
SplitRule.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
StateMonad.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
StringOrd.thy
|
Port AutoCorres to Isabelle 2014-RC0
|
2014-08-08 17:29:54 +10:00 |
SubMonadLib.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
TSubst.thy
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
Time_Methods_Cmd.thy
|
lib: refactor time_methods and test cases
|
2018-05-21 14:30:00 +10:00 |
Time_Methods_Cmd_Test.thy
|
lib/time_methods: add subseq example
|
2018-06-06 14:39:03 +10:00 |
Trace_Attribs.thy
|
lib/spec/proof/tools: fix word change fallout
|
2016-05-16 21:11:40 +10:00 |
Try_Methods.thy
|
Add some methods to trym.
|
2017-10-27 13:39:32 +11:00 |
TypHeapLib.thy
|
x64: merge master
|
2017-07-21 11:27:12 +10:00 |
Value_Abbreviation.thy
|
Add command/keyword 'value_abbreviation'.
|
2017-10-12 12:44:45 +11:00 |
WPTutorial.thy
|
trivial: fix missing dependency in WPTutorial
|
2017-01-31 08:42:08 +11:00 |
XPres.thy
|
remove most tab characters
|
2017-10-20 14:22:36 +11:00 |
continue.ML
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
crunch-cmd.ML
|
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
2018-06-26 14:45:28 +10:00 |
defs.ML
|
license-tool: missing license headers + .licenseignore [VER-551]
|
2016-07-14 16:34:31 +10:00 |
more_xml.ML
|
attribute tracing: Mechanism to work out changes in simpsets across revisions.
|
2014-10-13 11:05:31 +11:00 |
set.ML
|
lib: set: Add "filter" function for sets.
|
2014-12-03 14:49:12 +11:00 |
show_abbrevs.ML
|
Removes all trailing whitespaces
|
2017-07-12 15:13:51 +10:00 |
trace_attribs.ML
|
lib/spec/proof/tools: fix word change fallout
|
2016-05-16 21:11:40 +10:00 |