Diffusion afp-devel 5978c17604c0

merge from afp-2020
5978c17604c0
Actions

Tags

None

Subscribers

None

Description

merge from afp-2020

Details

Provenance

Authored on

Parents

rAFP9449ae539c8a: adapted to Isabelle2020-RC5
rAFP9a2a0d63ca30: fixed a frac_le proof

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFP5978c17604c0: merge from afp-2020.Apr 13 2020, 10:22 AM

Merged Changes

9a2a0d63ca30 fixed a frac_le proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
eea502832a73 fixed a failing frac_le proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ddaf86ffa226 merged
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
744b282fd492 updated benchmarks
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
819a553f7508 using proper atomic propositions, added more benchmarks
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
bde08698d726 avoid nonterminal clash in syntax translation
Author
traytel
Browse Repository
No Builds
No Audits
a0d561998f20 closed branch
Author
kleing
Browse Repository
No Builds
No Audits
8e995d947fb0 closed pull-request branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
249c2b58d173 closed merged branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
ad14484777fc merged
Author
gerwin.klein@nicta.com.au
Browse Repository
No Builds
No Audits
e3e858bfc9eb merged
Author
kleing
Browse Repository
No Builds
No Audits
4bea345493dd Closed branch ltl
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits
53421953ad96 WIP/LTL Entry
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (77)

Path

Size

etc/

metadata/

templates/

ArrowImpossibilityGS/

Thys/

Arrow_Order.thy

Auto2_HOL/

HOL/

Buchi_Complementation/

DynamicArchitectures/

Configuration_Traces.thy

Gauss_Jordan/

List-Infinite/

CommonArith/

ListInf/

LocalLexing/

Derivations.thy

MFODL_Monitor_Optimized

Abstract_Monitor.thy

Code_Double.thy

Monitor_Code.thy

Monitor_Impl.thy

Optimized_Join.thy

Optimized_MTL.thy

Nat-Interval-Logic/

IL_IntervalOperators.thy

Probabilistic_Timed_Automata/

PTA_Reachability.thy

library/

QR_Decomposition/

Gram_Schmidt.thy

QR_Decomposition.thy

Saturation_Framework

Consequence_Relations_and_Inference_Systems.thy

Labeled_Lifting_to_Non_Ground_Calculi.thy

Lifting_to_Non_Ground_Calculi.thy

Prover_Architectures.thy

Sliding_Window_Algorithm

TortoiseHare/

Applicative_Lifting.html

Containers.html

Furstenberg_Topology.html

Generic_Join.html

IEEE_Floating_Point.html

MFODL_Monitor_Optimized.html

MFOTL_Monitor.html

Monad_Normalisation.html

Ordered_Resolution_Prover.html

Saturation_Framework.html

Sliding_Window_Algorithm.html

Well_Quasi_Orders.html

statistics.html

rAFP5978c17604c0

etc/version

Loading...

metadata/metadata

Loading...

metadata/releases

Loading...

metadata/templates/using.tpl

Loading...

metadata/topics

Loading...

thys/ArrowImpossibilityGS/Thys/Arrow_Order.thy

Loading...

thys/Auto2_HOL/HOL/Arith_Thms.thy

Loading...

thys/Buchi_Complementation/Ranking.thy

Loading...

thys/DynamicArchitectures/Configuration_Traces.thy

Loading...

thys/Gauss_Jordan/Rank.thy

Loading...

thys/List-Infinite/CommonArith/Util_Nat.thy

Loading...

thys/List-Infinite/ListInf/List2.thy

Loading...

thys/LocalLexing/Derivations.thy

Loading...

thys/LocalLexing/Ladder.thy

Loading...

thys/LocalLexing/TheoremD10.thy

Loading...

thys/MFODL_Monitor_Optimized/Abstract_Monitor.thy

Loading...

thys/MFODL_Monitor_Optimized/Code_Double.thy

Loading...

thys/MFODL_Monitor_Optimized/Event_Data.thy

Loading...

thys/MFODL_Monitor_Optimized/Formula.thy

Loading...

thys/MFODL_Monitor_Optimized/Interval.thy

Loading...

thys/MFODL_Monitor_Optimized/Monitor.thy

Loading...

thys/MFODL_Monitor_Optimized/Monitor_Code.thy

Loading...

thys/MFODL_Monitor_Optimized/Monitor_Impl.thy

Loading...

thys/MFODL_Monitor_Optimized/Optimized_Join.thy

Loading...

thys/MFODL_Monitor_Optimized/Optimized_MTL.thy

Loading...

thys/MFODL_Monitor_Optimized/ROOT

Loading...

thys/MFODL_Monitor_Optimized/Regex.thy

Loading...

thys/MFODL_Monitor_Optimized/Trace.thy

Loading...

thys/MFODL_Monitor_Optimized/document/root.bib

Loading...

thys/MFODL_Monitor_Optimized/document/root.tex

Loading...

thys/Nat-Interval-Logic/IL_IntervalOperators.thy

Loading...

thys/Probabilistic_Timed_Automata/PTA_Reachability.thy

Loading...

thys/Probabilistic_Timed_Automata/library/Basic.thy

Loading...

thys/QR_Decomposition/Gram_Schmidt.thy

Loading...

thys/QR_Decomposition/QR_Decomposition.thy

Loading...

thys/ROOTS

Loading...

thys/Saturation_Framework/Calculi.thy

Loading...

thys/Saturation_Framework/Consequence_Relations_and_Inference_Systems.thy

Loading...

thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy

Loading...

thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy

Loading...

thys/Saturation_Framework/Prover_Architectures.thy

Loading...

thys/Saturation_Framework/ROOT

Loading...

thys/Saturation_Framework/document/auto/root.el

Loading...

thys/Saturation_Framework/document/root.tex

Loading...

thys/Sliding_Window_Algorithm/ROOT

Loading...

thys/Sliding_Window_Algorithm/SWA.thy

Loading...

thys/Sliding_Window_Algorithm/document/root.bib

Loading...

thys/Sliding_Window_Algorithm/document/root.tex

Loading...

thys/TortoiseHare/Brent.thy

Loading...

web/entries/Applicative_Lifting.html

Loading...

web/entries/BNF_CC.html

Loading...

web/entries/Containers.html

Loading...

web/entries/Furstenberg_Topology.html

Loading...

web/entries/Generic_Join.html

Loading...

web/entries/IEEE_Floating_Point.html

Loading...

web/entries/MFODL_Monitor_Optimized.html

Loading...

web/entries/MFOTL_Monitor.html

Loading...

web/entries/Monad_Normalisation.html

Loading...

web/entries/Ordered_Resolution_Prover.html

Loading...

web/entries/Saturation_Framework.html

Loading...

web/entries/Sliding_Window_Algorithm.html

Loading...

web/entries/Well_Quasi_Orders.html

Loading...

web/index.html

Loading...

web/rss.xml

Loading...

web/statistics.html

Loading...

web/topics.html

Loading...

web/using.html

Loading...