..
Hoare_Sep_Tactics
lib/sep_algebra: 2015 update
2015-05-14 11:40:55 +02:00
clib
Repair refine/crefine for WCET annotations.
2015-07-14 14:23:29 +10:00
doc
Import release snapshot.
2014-07-14 21:32:44 +02:00
ml-helpers
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
sep_algebra
lib/sep_algebra: 2015 update
2015-05-14 11:40:55 +02:00
subgoal_focus
Removed unused "Noting"
2015-07-08 17:05:19 +10:00
wp
Merge branch 'master' into aep-merge
2015-09-10 17:06:45 +10:00
Aligned.thy
fewer warnings
2015-05-16 19:52:49 +10:00
Apply_Trace.thy
start work on Isabelle 2015 update
2015-04-17 16:19:32 +01:00
Apply_Trace_Cmd.thy
start work on Isabelle 2015 update
2015-04-17 16:19:32 +01: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
Proof updates, working as far as AInvs.
2014-08-11 14:50:56 +10:00
Bisim_UL.thy
some of the global Isabelle2014 renames
2014-08-09 15:39:20 +10:00
CTranslationNICTA.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
Corres_UL.thy
fewer warnings
2015-05-16 19:52:49 +10:00
Crunch.ML
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
Crunch.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
Crunch_Test.thy
ported lib/* theories to Isabelle2014-RC0
2014-08-09 21:08:47 +10: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
fewer warnings
2015-05-16 19:52:49 +10:00
DistinctPropLemmaBucket.thy
fewer warnings
2015-05-16 19:52:49 +10:00
Distinct_Cmd.thy
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
Eisbach_Compat.thy
Added hotfix for rule instantiation attributes (of/where)
2015-07-08 16:58:14 +10:00
Eisbach_Methods.thy
remove NonDetMonad from C-Parser import chain
2015-07-09 14:47:25 +10:00
EmptyFailLib.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
Enumeration.thy
fewer warnings
2015-05-16 19:52:49 +10:00
EquivValid.thy
infoflow: Move "EquivValid" out of "infoflow/", into "lib/".
2014-10-13 11:05:31 +11:00
ExpandAll.thy
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
ExtraCorres.thy
Move some more lemmas into lib.
2014-07-18 17:23:07 +10: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
fewer warnings
2015-05-16 19:52:49 +10:00
HaskellLemmaBucket.thy
fewer warnings
2015-05-16 19:52:49 +10:00
HaskellLib_H.thy
GHC 7.8 update (bitSize -> finiteBitSize)
2014-11-28 08:58:57 +11:00
LemmaBucket.thy
lib: Some more trivial map-related lemmas.
2015-08-15 12:17:26 +10:00
LemmaBucket_C.thy
clib: 2015 update
2015-05-17 22:24:25 +10:00
Lib.thy
fewer warnings
2015-05-16 19:52:49 +10:00
ListLibLemmas.thy
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
List_Lib.thy
fewer warnings
2015-05-16 19:52:49 +10: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
ported lib/* theories to Isabelle2014-RC0
2014-08-09 21:08:47 +10:00
MoreDivides.thy
Port AutoCorres to Isabelle 2014-RC0
2014-08-08 17:29:54 +10:00
NICTACompat.thy
Added hotfix for rule instantiation attributes (of/where)
2015-07-08 16:58:14 +10:00
NICTATools.thy
Point to correct (existing) Rule_By_Method
2015-07-08 16:59:40 +10:00
NonDetMonadLemmaBucket.thy
fewer warnings
2015-05-16 19:52:49 +10:00
OptionMonad.thy
Port AutoCorres to Isabelle 2014-RC0
2014-08-08 17:29:54 +10:00
OptionMonadND.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
OptionMonadWP.thy
some of the global Isabelle2014 renames
2014-08-09 15:39:20 +10:00
Rule_By_Method.thy
Added Rule_By_Method (@ and # attributes)
2015-07-08 15:44:33 +10:00
SIMPL_Lemmas.thy
clib: 2015 update
2015-05-17 22:24:25 +10:00
SignedWords.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
SimpStrategy.thy
lib: more 2015 update
2015-05-09 13:03:30 +02:00
SimplRewrite.thy
clib: 2015 update
2015-05-17 22:24:25 +10:00
Simulation.thy
fewer warnings
2015-05-16 19:52:49 +10:00
Solves_Tac.thy
lib: Add "solves" tactic.
2014-12-01 11:08:34 +11:00
SpecValid_R.thy
fewer warnings
2015-05-16 19:52:49 +10:00
SplitRule.thy
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
StateMonad.thy
fewer warnings
2015-05-16 19:52:49 +10:00
StringOrd.thy
Port AutoCorres to Isabelle 2014-RC0
2014-08-08 17:29:54 +10:00
SubMonadLib.thy
fewer warnings
2015-05-16 19:52:49 +10:00
TSubst.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
Trace_Attribs.thy
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
TypHeapLib.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
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI
2015-04-18 21:51:26 +01:00
WhileLoopRulesCompleteness.thy
fewer warnings
2015-05-16 19:52:49 +10:00
WordBitwiseSigned.thy
lib: Add 'word_bitwise_signed' tactic.
2014-11-20 14:48:36 +11:00
WordEnum.thy
fewer warnings
2015-05-16 19:52:49 +10:00
WordLemmaBucket.thy
WordLemmaBucket: mehr lemma ist mehr gut
2015-08-19 15:14:31 +10:00
WordLib.thy
fewer warnings
2015-05-16 19:52:49 +10:00
WordSetup.thy
fewer warnings
2015-05-16 19:52:49 +10: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
lib: fewer warnings in crunch and wps
2015-05-16 21:46:45 +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
Import release snapshot.
2014-07-14 21:32:44 +02:00
trace_attribs.ML
attribute tracing: Mechanism to work out changes in simpsets across revisions.
2014-10-13 11:05:31 +11:00