..
ARM
lib: fix theory includes for arch-splitted WordSetup
2016-05-20 13:55:12 +10:00
Hoare_Sep_Tactics
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
Monad_WP
make strengthen method Eisbach-compatible
2017-03-21 11:15:04 +11:00
Word_Lib
lib: add definition for word_ctz (count trailing zeros)
2017-02-22 06:54:59 +11:00
X64
licenses: Updated licenses added from x64 backport
2017-02-28 12:26:19 +11:00
clib
update references from/to moved crefine, parametrise over L4V_ARCH
2017-03-31 16:13:41 +11: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
sep_algebra: add ROOT + regression test
2017-01-27 09:17:23 +01:00
subgoal_focus
license-tool: missing license headers + .licenseignore [VER-551]
2016-07-14 16:34:31 +10:00
AddUpdSimps.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
AdjustSchematic.thy
lib: move unused theory out of Monad_WP
2016-05-16 21:11:40 +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
apply_trace: general interface for printing
2017-02-15 15:00:23 +11:00
Apply_Trace_Cmd.thy
apply_trace: remove accidental reference to foo locale
2017-02-16 10:51:59 +11:00
AutoLevity.thy
regression: add test to check theory import paths
2016-05-27 16:17:13 +10:00
AutoLevity_Base.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
AutoLevity_Hooks.thy
added missing license headers
2016-06-23 14:02:41 +10:00
AutoLevity_Run.thy
autolevity: add support for per-apply lemma dependency tracking
2016-06-23 14:02:40 +10:00
AutoLevity_Test.thy
added missing license headers
2016-06-23 14:02:41 +10:00
AutoLevity_Theory_Report.thy
autolevity: refine tracing apply everywhere to work via Proof module hooks
2016-06-23 14:02:40 +10:00
BCorres_UL.thy
wp_cleanup: update proofs for new wp behaviour
2017-01-13 14:04:15 +01:00
Bisim_UL.thy
wp_cleanup: update proofs for new wp behaviour
2017-01-13 14:04:15 +01:00
BitFieldProofsLib.thy
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
CTranslationNICTA.thy
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
Conjuncts.thy
added optional "accumulate" flag to conjuncts to be used for multi-thms
2016-03-04 19:03:45 +11:00
Corres_Method.thy
corres_method: remove corres_concrete_P, reorder preconditions
2017-03-28 22:30:01 +11:00
Corres_Test.thy
corres_method: add some documentation
2017-03-28 22:30:02 +11:00
Corres_UL.thy
wp_cleanup: update proofs for new wp behaviour
2017-01-13 14:04:15 +01:00
Crunch.ML
Refactor of crunch.
2016-08-24 15:53:53 +10:00
Crunch.thy
Refactor of crunch.
2016-08-24 15:53:53 +10:00
Crunch_Test.thy
Refactor of crunch.
2016-08-24 15:53:53 +10:00
Crunch_Test_Qualified.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
DataMap.thy
SELFOUR-444: Adjust Haskell, new ghost data.
2016-11-02 11:19:09 +11:00
Defs.thy
trivial: fixups including some licence headers
2016-05-09 13:27:15 +10:00
Distinct_Cmd.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
Distinct_Prop.thy
Isabelle2016-1: update references to renamed constants and facts
2017-01-05 14:23:05 +11:00
Eisbach_Methods.thy
lib/eisbach_methods: make print_headgoal a primitive tactic
2017-03-28 21:51:57 +11:00
EmptyFailLib.thy
lib: start disentangling spaghetti word dependencies
2016-05-16 21:11:40 +10:00
EquivValid.thy
wp_cleanup: update proofs for new wp behaviour
2017-01-13 14:04:15 +01:00
Etanercept.thy
lib: arch-splitted WordSetup, fixed lib theory includes
2016-05-20 12:26:04 +10:00
ExpandAll.thy
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
Extend_Locale.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
ExtraCorres.thy
Isabelle2016-1: update references to renamed constants and facts
2017-01-05 14:23:05 +11:00
GenericLib.thy
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
GenericLib_C.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
HaskellLemmaBucket.thy
wp_cleanup: update proofs for new wp behaviour
2017-01-13 14:04:15 +01:00
HaskellLib_H.thy
VER-520: Change (>>) for (>>_)
2016-09-05 16:56:13 +10:00
Insulin.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
LemmaBucket.thy
lib: word and misc lemmas from SELFOUR-242 proofs
2017-02-09 15:05:52 +11:00
LemmaBucket_C.thy
c-parser: improve support for 64-bit platforms
2017-04-03 14:44:17 +10:00
Lib.thy
Isabelle2016-1: configure c-parser with faster string comparisons
2017-01-05 14:27:44 +11:00
ListLibLemmas.thy
Isabelle2016-1: expand uses of exists-unique with multiple binders
2017-01-05 14:26:56 +11:00
List_Lib.thy
Lib: Addition of auxiliary lemmas in basic theories to better support CRefine
2016-11-25 13:05:56 +11:00
MonadEq.thy
lib: start disentangling spaghetti word dependencies
2016-05-16 21:11:40 +10:00
MonadicRewrite.thy
wp_cleanup: update proofs for new wp behaviour
2017-01-13 14:04:15 +01:00
NICTATools.thy
apply_debug: include apply_debug by default
2017-02-15 15:00:23 +11:00
NonDetMonadLemmaBucket.thy
Isabelle2016-1: fix Word_Miscellaneous import path
2017-02-08 16:53:14 +11:00
ProvePart.thy
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
Qualify.thy
trivial: fixups including some licence headers
2016-05-09 13:27:15 +10:00
Requalify.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
Rule_By_Method.thy
lib/rule_by_method: add "atomized" attribute
2017-03-28 21:53:11 +11:00
SIMPL_Lemmas.thy
SELFOUR-444: CRefine proof for preemptible retype.
2016-11-02 11:19:09 +11:00
ShowTypes.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
SimpStrategy.thy
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11:00
SimplRewrite.thy
Isabelle2016-1: replace 'unfolded' attr with 'simplified' where the former now loops
2017-01-05 14:27:04 +11:00
Simulation.thy
fewer warnings
2015-05-16 19:52:49 +10:00
Solves_Tac.thy
license-tool: missing license headers + .licenseignore [VER-551]
2016-07-14 16:34:31 +10:00
SpecValid_R.thy
fewer warnings
2015-05-16 19:52:49 +10:00
SplitRule.thy
fix lib for isabelle 2016
2016-01-12 14:58:16 +11:00
StateMonad.thy
lib: unbitrotted StateMonad
2016-05-16 21:11:40 +10:00
StringOrd.thy
Port AutoCorres to Isabelle 2014-RC0
2014-08-08 17:29:54 +10:00
String_Compare.thy
Isabelle2016-1: add support for faster string comparisons
2017-01-05 14:27:41 +11:00
SubMonadLib.thy
Isabelle2016-1: fix proofs involving UNION
2017-01-05 14:27:33 +11:00
TSubst.thy
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
Trace_Attribs.thy
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
TypHeapLib.thy
c-parser: improve support for 64-bit platforms
2017-04-03 14:44:17 +10:00
WPTutorial.thy
trivial: fix missing dependency in WPTutorial
2017-01-31 08:42:08 +11: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
Isabelle2016-1: update to new ML API
2017-01-05 14:26:14 +11: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
Import release snapshot.
2014-07-14 21:32:44 +02:00
trace_attribs.ML
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00