l4v/lib at master · seL4/l4v

History

Name		Name	Last commit message	Last commit date
parent directory ..
Basics		Basics
CorresK		CorresK
EVTutorial		EVTutorial
Eisbach_Tools		Eisbach_Tools
Hoare_Sep_Tactics		Hoare_Sep_Tactics
ML_Utils		ML_Utils
Monads		Monads
Word_Lib		Word_Lib
clib		clib
concurrency		concurrency
sep_algebra		sep_algebra
test		test
AddUpdSimps.thy		AddUpdSimps.thy
BCorres_UL.thy		BCorres_UL.thy
Bisim_UL.thy		Bisim_UL.thy
CorresK_Method.thy		CorresK_Method.thy
CorresWhile.thy		CorresWhile.thy
Corres_Adjust_Preconds.thy		Corres_Adjust_Preconds.thy
Corres_Cases.thy		Corres_Cases.thy
Corres_Method.thy		Corres_Method.thy
Corres_UL.thy		Corres_UL.thy
Crunch.ML		Crunch.ML
Crunch.thy		Crunch.thy
Crunch_Instances_NonDet.thy		Crunch_Instances_NonDet.thy
Crunch_Instances_Trace.thy		Crunch_Instances_Trace.thy
CutMon.thy		CutMon.thy
DataMap.thy		DataMap.thy
Defs.thy		Defs.thy
DetWPLib.thy		DetWPLib.thy
Distinct_Cmd.thy		Distinct_Cmd.thy
EquivValid.thy		EquivValid.thy
Eval_Bool.thy		Eval_Bool.thy
ExtraCorres.thy		ExtraCorres.thy
Extract_Conjunct.thy		Extract_Conjunct.thy
FP_Eval.thy		FP_Eval.thy
FastMap.thy		FastMap.thy
Find_Names.thy		Find_Names.thy
GenericLib.thy		GenericLib.thy
GenericTag.thy		GenericTag.thy
Guess_ExI.thy		Guess_ExI.thy
HaskellLemmaBucket.thy		HaskellLemmaBucket.thy
HaskellLib_H.thy		HaskellLib_H.thy
Heap_List.thy		Heap_List.thy
Injection_Handler.thy		Injection_Handler.thy
Insulin.thy		Insulin.thy
LemmaBucket.thy		LemmaBucket.thy
LexordList.thy		LexordList.thy
Lib.thy		Lib.thy
ListLibLemmas.thy		ListLibLemmas.thy
List_Lib.thy		List_Lib.thy
Locale_Abbrev.thy		Locale_Abbrev.thy
ML_Goal.thy		ML_Goal.thy
ML_Goal_Test.thy		ML_Goal_Test.thy
Match_Abbreviation.thy		Match_Abbreviation.thy
Monad_Commute.thy		Monad_Commute.thy
Monad_Lists.thy		Monad_Lists.thy
MonadicRewrite.thy		MonadicRewrite.thy
More_Numeral_Type.thy		More_Numeral_Type.thy
NICTATools.thy		NICTATools.thy
Named_Eta.thy		Named_Eta.thy
NonDetMonadLemmaBucket.thy		NonDetMonadLemmaBucket.thy
None_Top_Bot.thy		None_Top_Bot.thy
Oblivious.thy		Oblivious.thy
Qualify.thy		Qualify.thy
RCorres.thy		RCorres.thy
ROOT		ROOT
RangeMap.thy		RangeMap.thy
Repeat_Attribute.thy		Repeat_Attribute.thy
Requalify.thy		Requalify.thy
Rules_Tac.thy		Rules_Tac.thy
ShowTypes.thy		ShowTypes.thy
SimpStrategy.thy		SimpStrategy.thy
Simulation.thy		Simulation.thy
Solves_Tac.thy		Solves_Tac.thy
Sorted_Addrs.thy		Sorted_Addrs.thy
SpecValid_R.thy		SpecValid_R.thy
SplitRule.thy		SplitRule.thy
StateMonad.thy		StateMonad.thy
SubMonadLib.thy		SubMonadLib.thy
Time_Methods_Cmd.thy		Time_Methods_Cmd.thy
Try_Attribute.thy		Try_Attribute.thy
Try_Methods.thy		Try_Methods.thy
Value_Abbreviation.thy		Value_Abbreviation.thy
Value_Type.thy		Value_Type.thy
crunch-cmd.ML		crunch-cmd.ML
defs.ML		defs.ML
set.ML		set.ML
tests.xml		tests.xml

Navigation Menu

Uh oh!

Uh oh!

FilesExpand file tree

lib

Directory actions

More options

Directory actions

More options

Latest commit

History

lib

Folders and files

parent directory