Diffusion afp-devel e39f7649d57a

merged from afp-2019
e39f7649d57a
Actions

Tags

None

Subscribers

None

Description

merged from afp-2019

Details

Provenance

Authored on

Parents

rAFP38874e3c4e3d: more Logic reorg
rAFP92b287f467d0: merged commit from afp-devel

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFPe39f7649d57a: merged from afp-2019.Apr 13 2020, 5:57 AM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

92b287f467d0 merged commit from afp-devel
Author
kleing
Browse Repository
No Builds
No Audits
b3fb5b59b92e 2019 -> 2020 in docs
Author
kleing
Browse Repository
No Builds
No Audits
d2b8bb8390f7 update tar.gz releases
Author
kleing
Browse Repository
No Builds
No Audits
2df1c25ed806 set version to 2020
Author
kleing
Browse Repository
No Builds
No Audits
846453287399 Backed out changesets 4424bf5e28e0, 6bdf58e7175e, 9bd18ac101a7 for Isabelle2020
Author
kleing
Browse Repository
No Builds
No Audits
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
81ec186eae5e Fixed some typos in Furstenberg_Topology
Author
pruvisto
Browse Repository
No Builds
No Audits
9ff984debb46 merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
deab09fedc87 Grant acknowledgement for ALEXANDRIA (ERC Project 742178)
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c00714f311dc Update abstract
Author
Asta Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
8e310d6353b2 Update websites and emails.
Author
Asta Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
057bf095850f improved estimation by getting rid of max-1 operation in…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
4424bf5e28e0 more fixes for alias issues (which for Auto2 means giving up)
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
6bdf58e7175e elimination of some aliases
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
9bd18ac101a7 elimination of some aliases, etc.
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
1093d9d3d61f Completed list of rules for differential invariance.
Author
Jonathan Julian Huerta y Munive <jonjulian23@gmail.com>
Browse Repository
No Builds
No Audits
d556b9b6d06a Some new and/or generalised theorems
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c210ece1391e Word_Lib: document build
Author
kleing
Browse Repository
No Builds
No Audits
16b636683e92 Word_Lib: contributions from l4v
Author
kleing
Browse Repository
No Builds
No Audits
de0c57e464f7 revert change to ~~ syntax
Author
kleing
Browse Repository
No Builds
No Audits
226a441efab0 added a few lemmas to Stone_Kleene_Relation_Algebras
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
0e0a6e473852 Substitution in LTL DNF formulas
Author
Benedikt Seidl <benedikt.seidl@tum.de>
Browse Repository
No Builds
No Audits
3eba78a12810 fixed some TeX problems
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
6f20a9c4c987 ZFC_in_HOL: Now with Cantor normal form!
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
171b62f0789a A new lemma
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
7c537805ccf2 some new lemmas
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
23d7d61fa263 proper escape for literal single quotes;
Author
makarius
Browse Repository
No Builds
No Audits
d4e2b44208ee tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
1a10a02abc03 avoid hardwired document preparation;
Author
makarius
Browse Repository
No Builds
No Audits
efef42e4851d cited ITP paper
Author
Akihisa Yamada <akihisa.yamada@uibk.ac.at>
Browse Repository
No Builds
No Audits
792d392d112d Added revision meta-data for Optics.
Author
Simon Foster <simon.foster@york.ac.uk>
Browse Repository
No Builds
No Audits
44e2e5c9f328 Added partial bijective and symmetric lenses. Improved alphabet command…
Author
Simon Foster <simon.foster@york.ac.uk>
Browse Repository
No Builds
No Audits
b8e1eebb4b17 merge
Author
Asta Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
f5a944f4cf54 Add inputenc
Author
Asta Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
27ea89db8cd6 continued working on automata tool and benchmarks
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
89ba7ebaf43f New and/or strengthened lemmas
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
76aa4d49a895 Demote some simps that were not pulling their weight.
Author
"Eugene W. Stark <stark@cs.stonybrook.edu>"
Browse Repository
No Builds
No Audits
4b4d09cb8a4c Tweaks, mostly in search of speedup.
Author
"Eugene W. Stark <stark@cs.stonybrook.edu>"
Browse Repository
No Builds
No Audits
2d4667e525c2 merged
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
cd0b90f7688d added equivalence and automata tool
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
6119bf12038f streamlined NBA translation
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
bf1920e1bc60 make Poincare_Disc build on Complex_Geometry
Author
pruvisto
Browse Repository
No Builds
No Audits
c35f8cc3dda7 repaired broken proofs in Skip_Lists; removed unfinished experimental thy file
Author
pruvisto
Browse Repository
No Builds
No Audits
29f2271f9455 a few new lemmas
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c9a73112a393 updated root file
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits

Changes (57)

Path

Size

metadata/

MFODL_Monitor_Optimized

Abstract_Monitor.thy

Code_Double.thy

Monitor_Code.thy

Monitor_Impl.thy

Optimized_Join.thy

Optimized_MTL.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

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

rAFPe39f7649d57a

metadata/metadata

Loading...

metadata/topics

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/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...

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...