adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/lib
History
Thomas Sewell caf0529c7f Move burden of 'halt' proof, use less modifies. 
In detail:
  - add a general user-specified exception to c_exntype
    (for use in tools like Substitute)
  - wrap calls to 'halt' in Guard {}, making it clearer that
    halt is never called, simplifying asmrefine
  - repair halt changes in crefine
  - avoid use of some suspicious 'modifies' properties in crefine
    which were generated by the parser for functions where inline
    ASM blocks have been elided, and which may be inaccurate.
 		2014-08-29 13:57:28 +10:00
..
Hoare_Sep_Tactics Import release snapshot. 2014-07-14 21:32:44 +02:00
clib remove old levity and taint-mode comments 2014-07-22 18:10:28 +02:00
doc Import release snapshot. 2014-07-14 21:32:44 +02:00
eisbach Import release snapshot. 2014-07-14 21:32:44 +02:00
ml-helpers Import release snapshot. 2014-07-14 21:32:44 +02:00
proof_counting Import release snapshot. 2014-07-14 21:32:44 +02:00
sep_algebra release cleanup 2014-07-17 18:22:50 +02:00
wp autocorres: Remove unnecessary rule from "whileLoop_results". 2014-08-13 12:18:46 +10:00
Aligned.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Apply_Trace.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Apply_Trace_Cmd.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
AutoLevity.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
AutoLevity_Run.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
BCorres_UL.thy comment cleanup 2014-07-22 18:10:20 +02:00
Bisim_UL.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
CTranslationNICTA.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
CodeArbitrary.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Corres_UL.thy release cleanup 2014-07-17 18:22:50 +02:00
Crunch.ML comment cleanup 2014-07-22 18:10:20 +02:00
Crunch.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Crunch_Test.thy comment cleanup 2014-07-22 18:10:20 +02:00
Crunch_Test_Qualified.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
DataMap.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
DistinctProp.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
DistinctPropLemmaBucket.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
EmptyFailLib.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Enumeration.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
ExpandAll.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
ExtraCorres.thy Move some more lemmas into lib. 2014-07-18 17:23:07 +10:00
Focus.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
GenericLib.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
GenericLib_C.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
HOLLemmaBucket.thy release cleanup 2014-07-17 18:22:50 +02:00
HaskellLemmaBucket.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
HaskellLib_H.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
LemmaBucket.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
LemmaBucket_C.thy SIMPL->Graph proofs largely working. 2014-08-27 15:30:34 +10:00
Lib.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
ListLibLemmas.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
List_Lib.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Methods.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
MonadEq.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
MonadicRewrite.thy release cleanup 2014-07-17 18:22:50 +02:00
MoreDivides.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
NICTACompat.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
NICTATools.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
NonDetMonadLemmaBucket.thy Fix previous commit. 2014-07-19 00:04:21 +10:00
OptionMonad.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
OptionMonadND.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
OptionMonadWP.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
SIMPL_Lemmas.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
SignedWords.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
SimpStrategy.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
SimplRewrite.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Simulation.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
SpecValid_R.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
SplitRule.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
StateMonad.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
StringOrd.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
SubMonadLib.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
TSubst.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
TypHeapLib.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Upto.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
WPTutorial.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
WhileLoopRules.thy autocorres: Remove unnecessary rule from "whileLoop_results". 2014-08-13 12:18:46 +10:00
WhileLoopRulesCompleteness.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
WordEnum.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
WordLemmaBucket.thy Fix previous commit. 2014-07-19 00:04:21 +10:00
WordLib.thy Move burden of 'halt' proof, use less modifies. 2014-08-29 13:57:28 +10:00
WordSetup.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
XPres.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
continue.ML Import release snapshot. 2014-07-14 21:32:44 +02:00
crunch-cmd.ML comment cleanup 2014-07-22 18:10:20 +02:00
show_abbrevs.ML Import release snapshot. 2014-07-14 21:32:44 +02:00