adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/lib
History
Japheth Lim a4878ccb2b lib: move crunch tests to LibTest session 2018-09-27 15:03:24 +10:00
..
ARM lib/Word_Lib: use qualified session imports 2018-08-20 09:05:52 +10:00
ARM_HYP lib/Word_Lib: use qualified session imports 2018-08-20 09:05:52 +10:00
Hoare_Sep_Tactics lib+sysinit: add extended separation algebra and forward reasoning tactics 2018-09-18 12:01:52 +10:00
Monad_WP Isabelle2018: Lib update 2018-08-20 09:06:36 +10:00
RISCV64 globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
Word_Lib lib: trivial: remove trailing whitespace in root.tex 2018-08-21 15:46:03 +10:00
X64 lib/Word_Lib: use qualified session imports 2018-08-20 09:05:52 +10:00
clib lib/clib: move DetWPLib from CLib to Lib 2018-08-20 09:06:37 +10:00
concurrency Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
doc Import release snapshot. 2014-07-14 21:32:44 +02:00
ml-helpers Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
sep_algebra lib+sysinit: add extended separation algebra and forward reasoning tactics 2018-09-18 12:01:52 +10:00
subgoal_focus Isabelle2018: Subgoal_Methods update 2018-08-20 09:06:36 +10:00
AddUpdSimps.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
AdjustSchematic.thy globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
Apply_Debug.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Apply_Debug_Test.thy apply_debug: fix example in tutorial 2017-02-15 15:00:23 +11:00
Apply_Trace.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Apply_Trace_Cmd.thy Removes all trailing whitespaces 2017-07-12 15:13:51 +10:00
AutoLevity.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
AutoLevity_Base.thy Isabelle2017: update lib for RC0 2017-10-30 12:23:26 +11:00
AutoLevity_Hooks.thy lib: change where temp file for AutoLevity tracing is created 2018-07-04 19:24:36 +10:00
AutoLevity_Test.thy Removes all trailing whitespaces 2017-07-12 15:13:51 +10:00
AutoLevity_Theory_Report.thy Isabelle2018: Lib update 2018-08-20 09:06:36 +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 Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Conjuncts.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
CorresK_Lemmas.thy Isabelle2018: Lib update 2018-08-20 09:06:36 +10:00
Corres_Adjust_Preconds.thy Add some comments. 2017-08-04 11:28:54 +10:00
Corres_Method.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Corres_Test.thy Isabelle2018: Lib update 2018-08-20 09:06:36 +10:00
Corres_UL.thy Isabelle2018: Lib update 2018-08-20 09:06:36 +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: move crunch tests to LibTest session 2018-09-27 15:03:24 +10:00
Crunch_Test_Qualified_NonDet.thy lib: move crunch tests to LibTest session 2018-09-27 15:03:24 +10:00
Crunch_Test_Qualified_Trace.thy lib: move crunch tests to LibTest session 2018-09-27 15:03:24 +10:00
Crunch_Test_Trace.thy lib: move crunch tests to LibTest session 2018-09-27 15:03:24 +10:00
DataMap.thy globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
Defs.thy Removes all trailing whitespaces 2017-07-12 15:13:51 +10:00
DetWPLib.thy lib/clib: move DetWPLib from CLib to Lib 2018-08-20 09:06:37 +10:00
Distinct_Cmd.thy Isabelle2016-1: update to new ML API 2017-01-05 14:26:14 +11:00
Distinct_Prop.thy lib/Word_Lib: use qualified session imports 2018-08-20 09:05:52 +10:00
Eisbach_Methods.thy lib: add method to shorthand larger methods 2018-09-14 16:35:27 +10:00
EmptyFailLib.thy Removes all trailing whitespaces 2017-07-12 15:13:51 +10:00
EquivValid.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Eval_Bool.thy lib: Change Add_Locale_Code_Defs to filter out rules with sort hypotheses. 2018-08-14 11:32:31 +10:00
ExpandAll.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Extend_Locale.thy Isabelle2018: Extend_Locale update 2018-08-20 09:06:36 +10:00
ExtraCorres.thy lib/wp: Remove old wp combinator rules. 2018-03-16 14:51:31 +11:00
Extract_Conjunct.thy Isabelle2018: new comment syntax 2018-08-20 09:06:35 +10: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
HaskellLemmaBucket.thy Isabelle2018: Lib update 2018-08-20 09:06:36 +10:00
HaskellLib_H.thy lib: change runErrorT to runExceptT to match Haskell code 2018-09-04 14:59:45 +10:00
Insulin.thy lib: add license header text 2018-09-27 15:03:24 +10:00
Insulin_Test.thy lib: test cases for Insulin and ShowTypes tools 2018-09-27 15:03:24 +10:00
LemmaBucket.thy Word_Lib: consolidate LemmaBucket and Lib lemmas into Word_Lib 2018-08-20 09:06:36 +10:00
LexordList.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Lib.thy Word_Lib: consolidate LemmaBucket and Lib lemmas into Word_Lib 2018-08-20 09:06:36 +10:00
ListLibLemmas.thy Removes all trailing whitespaces 2017-07-12 15:13:51 +10:00
List_Lib.thy globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
Local_Method.thy lib: add method to shorthand larger methods 2018-09-14 16:35:27 +10:00
Local_Method_Tests.thy lib: move test theories in Lib to LibTest 2018-09-14 16:35:27 +10:00
Match_Abbreviation.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +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 Isabelle2018: Lib update 2018-08-20 09:06:36 +10:00
NICTATools.thy lib: Add attribute to ignore errors (VER-1007) 2018-09-19 11:57:19 +10:00
NonDetMonadLemmaBucket.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
ProvePart.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Qualify.thy Isabelle2017: update lib for RC0 2017-10-30 12:23:26 +11:00
Qualify_Test.thy lib: test cases for Qualify tool 2018-09-27 15:03:24 +10:00
ROOT lib: move crunch tests to LibTest session 2018-09-27 15:03:24 +10:00
Requalify.thy Isabelle2018 lib: requalify facts up to pattern equivalence 2018-08-20 09:06:36 +10:00
Rule_By_Method.thy globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
ShowTypes.thy lib: add license header text 2018-09-27 15:03:24 +10:00
ShowTypes_Test.thy lib: test cases for Insulin and ShowTypes tools 2018-09-27 15:03:24 +10:00
SimpStrategy.thy globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
Simp_No_Conditional.thy lib: add non-cond-simplification, use in wpsimp. 2018-08-03 18:25:30 +10:00
Simulation.thy Isabelle2018: new comment syntax 2018-08-20 09:06:35 +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 globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
StateMonad.thy lib: fix unused/historical StateMonad theory 2018-08-20 09:05:52 +10:00
StringOrd.thy globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
SubMonadLib.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
TSubst.thy Removes all trailing whitespaces 2017-07-12 15:13:51 +10:00
Time_Methods_Cmd.thy lib: time_methods: add flag to skip failure output 2018-09-14 16:35:27 +10:00
Time_Methods_Cmd_Test.thy lib: time_methods: add flag to skip failure output 2018-09-14 16:35:27 +10:00
Trace_Attribs.thy lib/spec/proof/tools: fix word change fallout 2016-05-16 21:11:40 +10:00
Trace_Schematic_Insts.thy lib/Trace_Schematic_Insts: refactor; improve ML style 2018-08-16 14:21:16 +10:00
Trace_Schematic_Insts_Test.thy lib: add Trace_Schematic_Insts_Test to LibTest 2018-09-27 15:03:24 +10:00
Try_Attribute.thy lib: TRY attribute: handle more errors 2018-09-20 18:17:23 +10:00
Try_Methods.thy Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
Value_Abbreviation.thy Isabelle2018 lib: remove evaluator parameter for value_abbreviation 2018-08-20 09:06:36 +10:00
WPTutorial.thy lib: repair WPTutorial and CorresTest 2018-08-20 09:06:34 +10:00
continue.ML Removes all trailing whitespaces 2017-07-12 15:13:51 +10:00
crunch-cmd.ML lib/crunch: use induct package. 2018-08-03 12:20:49 +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
tests.xml Isabelle2018: record c-parser dependency for LibTest 2018-08-20 09:06:37 +10:00
trace_attribs.ML lib/spec/proof/tools: fix word change fallout 2016-05-16 21:11:40 +10:00