Diffusion afp-devel e760bb298ecd

merge from afp-2019
e760bb298ecd
Actions

Tags

None

Subscribers

None

Description

merge from afp-2019

Details

Provenance

Authored on

Parents

rAFP79e888fe281b: new entry Isabelle_C
rAFP139f5ffeed6f: Word_Lib: latex document fix

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFPe760bb298ecd: merge from afp-2019.Dec 19 2019, 8:30 AM

Merged Changes

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

139f5ffeed6f Word_Lib: latex document fix
Author
kleing
Browse Repository
No Builds
No Audits
4e2c2331b602 Word_Lib: cleanup, shorter proofs; new material from l4v; word_eqI method
Author
kleing
Browse Repository
No Builds
No Audits
0b9412db8759 made LFP operation more faithful to the implementation
Author
traytel
Browse Repository
No Builds
No Audits
bdb912acf555 remove left-over comment
Author
kleing
Browse Repository
No Builds
No Audits
2e0d1f786e12 added a sorting theory
Author
nipkow
Browse Repository
No Builds
No Audits
09bbfde13795 merge
Author
Giuliano Losa <giuliano@losa.fr>
Browse Repository
No Builds
No Audits
26189c7b6997 eliminate smt command at line 311
Author
Giuliano Losa <giuliano@losa.fr>
Browse Repository
No Builds
No Audits
ca5f1ca3a8e5 tuned
Author
nipkow
Browse Repository
No Builds
No Audits
dc000cacc8fa tuned
Author
nipkow
Browse Repository
No Builds
No Audits
9282ad6144da new theory in Priority_Queue_Braun
Author
nipkow
Browse Repository
No Builds
No Audits
fd8327b801a2 merged
Author
nipkow
Browse Repository
No Builds
No Audits
0e1e232a338a tuned
Author
nipkow
Browse Repository
No Builds
No Audits
aecde7853101 tuning
Author
blanchette
Browse Repository
No Builds
No Audits
04690e89d173 EPO: switch size measure
Author
Alexander Bentkamp <a.bentkamp@vu.nl>
Browse Repository
No Builds
No Audits
f9cbe0d87965 adapt to isabelle/a30278c8585f; tuned whitespace
Author
traytel
Browse Repository
No Builds
No Audits
712c4cf1b3c1 fixed a theory sensitive to ext_funcset_to_sing_iff
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
429a712d7c4d adapted to devel
Author
nipkow
Browse Repository
No Builds
No Audits
7c33f283cfef MPC update ETP and perfect sec rename
Author
davetbutler
Browse Repository
No Builds
No Audits
8c3387faaeed Fixed CAVA-Impl to accomodate for generalized Gabow_GBG
Author
peter_lammich
Browse Repository
No Builds
No Audits
3049a0ad195d merged
Author
peter_lammich
Browse Repository
No Builds
No Audits
7d5c0f2b46b5 Generalized Gabow-SCC to arbitrary refinements for nodes
Author
peter_lammich
Browse Repository
No Builds
No Audits
3768c25e32fa Removal of material that has been transferred to the main libraries
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
801b10285bb6 merged
Author
makarius
Browse Repository
No Builds
No Audits
de5e63a46b97 adapted to Isabelle/5727bcc3c47c;
Author
makarius
Browse Repository
No Builds
No Audits
5c040dde3c39 merge from 2019
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
9b2518d009e9 adapted to devel (Monda Syntax)
Author
nipkow
Browse Repository
No Builds
No Audits
fef8125d181c added directory-entry in ROOT file of VerifyThis2019 (when merging from AFP…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
e10739c4e48f merge from AFP 2019
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
e30fe5fba4d7 Merged
Author
pruvisto
Browse Repository
No Builds
No Audits
4f482d20a008 adapted to isabelle-dev 954ee5acaae0
Author
pruvisto
Browse Repository
No Builds
No Audits
e8bc925a7952 adapted to Isabelle/0c47c128f9af;
Author
Wenda Li <liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
7e45833c40f6 explicit variable declaration
Author
florian.haftmann
Browse Repository
No Builds
No Audits
78025c98b739 adapted to Isabelle/592e2afdd50c;
Author
makarius
Browse Repository
No Builds
No Audits
6128683958ca more realistic timeout;
Author
makarius
Browse Repository
No Builds
No Audits
c47ca19eaae3 proper prefix syntax
Author
florian.haftmann
Browse Repository
No Builds
No Audits
7e7b23d02d4b removed unused auxiliary lemmas
Author
florian.haftmann
Browse Repository
No Builds
No Audits
87c3943758c0 More about Bernoulli numbers
Author
pruvisto
Browse Repository
No Builds
No Audits
5580004cc074 Added von Staudt–Clausen theorem to Bernoulli
Author
pruvisto
Browse Repository
No Builds
No Audits
f1ef07c47429 don't build Linear_Programming on Mac
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
54f6a4f1d8a3 updated to fdb6c5034c24
Author
nipkow
Browse Repository
No Builds
No Audits
2a06a089800f merged
Author
immler
Browse Repository
No Builds
No Audits
c5944c920143 moved Interval and Interval_Approximation to isabelle
Author
immler
Browse Repository
No Builds
No Audits
3f2bdb753c38 patched a proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c5c88012f116 fixed a failing (and ugly) proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
1f17a5f5a1e2 Merge branch
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
f05300d8017a Tuned spacing.
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
877fab13602e follow devel changeset 581083959358
Author
nipkow
Browse Repository
No Builds
No Audits
1a0be182fdda Consistent spacing in set comprehension and name fixes.
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
616e41c5089c Consistent spacing in set comprehension.
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
ba01b2eda5e4 updated email
Author
nipkow
Browse Repository
No Builds
No Audits

Changes (180)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

Generalized_Counting_Sort

Conservation.thy

C_Appendices.thy

DOF-scholarly_paper.sty

DOF-technical_report.sty

DOF-scholarly_paper.sty

DOF-technical_report.sty

A-C-Source10.png

A-C-Source2.png

A-C-Source3.png

A-C-Source5.png

A-C-Source6.png

A-C-Source7.png

A-C-Source8.png

A-C-Source80.png

A-C-Source9.png

C-export-example.png

C11-Package-Architecture.pdf

document-model1.pdf

document-model2.pdf

markup-demo.png

c_grammar_fun.grm

c_grammar_fun.grm.sig

c_grammar_fun.grm.sml

C_Environment.thy

C_Lexer_Annotation.thy

C_Lexer_Language.thy

C_Parser_Annotation.thy

C_Parser_Language.thy

aligned_struct_c18.c

argument_scope.c

atomic_parenthesis.c

bitfield_declaration_ambiguity.c

bitfield_declaration_ambiguity.fail.c

bitfield_declaration_ambiguity.ok.c

char-literal-printing.c

control-scope.c

dangling_else.c

dangling_else_lookahead.c

dangling_else_lookahead.if.c

dangling_else_misleading.fail.c

declaration_ambiguity.c

declarator_visibility.c

enum_constant_visibility.c

enum_shadows_typedef.c

function-decls.c

function_parameter_scope.c

function_parameter_scope_extends.c

local_typedef.c

long-long-struct.c

no_local_scope.c

parameter_declaration_ambiguity.c

parameter_declaration_ambiguity.test.c

struct-recursion.c

variable_star.c

Poincare_Bendixson

Affine_Arithmetic_Misc.thy

Analysis_Misc.thy

Periodic_Orbit.thy

Poincare_Bendixson.thy

CISC-Kernel.html

Featherweight_OCL.html

Generalized_Counting_Sort.html

InfPathElimination.html

Isabelle_C.html

Isabelle_Meta_Model.html

Ordinary_Differential_Equations.html

Poincare_Bendixson.html

TESL_Language.html

UPF_Firewall.html

statistics.html

rAFPe760bb298ecd

metadata/metadata

thys/Generalized_Counting_Sort/Algorithm.thy

thys/Generalized_Counting_Sort/Conservation.thy

thys/Generalized_Counting_Sort/ROOT

thys/Generalized_Counting_Sort/Sorting.thy

thys/Generalized_Counting_Sort/Stability.thy

thys/Generalized_Counting_Sort/document/root.bib

thys/Generalized_Counting_Sort/document/root.tex

thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy

thys/Isabelle_C/C11-FrontEnd/C_Main.thy

thys/Isabelle_C/C11-FrontEnd/document/DOF-COL.sty

thys/Isabelle_C/C11-FrontEnd/document/DOF-core.sty

thys/Isabelle_C/C11-FrontEnd/document/DOF-scholarly_paper.sty

thys/Isabelle_C/C11-FrontEnd/document/DOF-technical_report.sty

thys/Isabelle_C/C11-FrontEnd/document/figures

thys/Isabelle_C/C11-FrontEnd/document/generated/DOF-COL.sty

thys/Isabelle_C/C11-FrontEnd/document/generated/DOF-core.sty

thys/Isabelle_C/C11-FrontEnd/document/generated/DOF-scholarly_paper.sty

thys/Isabelle_C/C11-FrontEnd/document/generated/DOF-technical_report.sty

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source10.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source2.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source3.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source5.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source6.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source7.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source8.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source80.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/A-C-Source9.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/C-export-example.png

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/C11-Package-Architecture.pdf

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/document-model1.pdf

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/document-model2.pdf

thys/Isabelle_C/C11-FrontEnd/document/generated/figures/markup-demo.png

thys/Isabelle_C/C11-FrontEnd/document/generated/ontologies.tex

thys/Isabelle_C/C11-FrontEnd/document/generated/paper.tex

thys/Isabelle_C/C11-FrontEnd/document/lstisadof.sty

thys/Isabelle_C/C11-FrontEnd/document/ontologies.tex

thys/Isabelle_C/C11-FrontEnd/document/paper.tex

thys/Isabelle_C/C11-FrontEnd/document/preamble.tex

thys/Isabelle_C/C11-FrontEnd/document/root.bib

thys/Isabelle_C/C11-FrontEnd/document/root.tex

thys/Isabelle_C/C11-FrontEnd/examples/C0.thy

thys/Isabelle_C/C11-FrontEnd/examples/C1.thy

thys/Isabelle_C/C11-FrontEnd/examples/C2.thy

thys/Isabelle_C/C11-FrontEnd/examples/C_paper.thy

thys/Isabelle_C/C11-FrontEnd/generated/c_ast.ML

thys/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm

thys/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm.sig

thys/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm.sml

thys/Isabelle_C/C11-FrontEnd/src/C_Ast.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Document.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Environment.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Eval.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Annotation.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Language.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Annotation.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy

thys/Isabelle_C/README.md

thys/Isabelle_C/README.thy

thys/Isabelle_C/ROOT

thys/Isabelle_C/src_ext/mlton/LICENSE

thys/Isabelle_C/src_ext/mlton/README.adoc

thys/Isabelle_C/src_ext/mlton/doc/license/MLKit-LICENSE

thys/Isabelle_C/src_ext/mlton/doc/license/MLton-LICENSE

thys/Isabelle_C/src_ext/mlton/doc/license/NEC-LICENSE

thys/Isabelle_C/src_ext/mlton/doc/license/NJ-LICENSE

thys/Isabelle_C/src_ext/mlton/doc/license/README

thys/Isabelle_C/src_ext/mlton/doc/license/gdtoa-LICENSE

thys/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/base.sig

thys/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/join.sml

thys/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/lrtable.sml

thys/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/parser1.sml

thys/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/stream.sml

thys/Isabelle_C/src_ext/mlton/mlyacc/COPYRIGHT

thys/Isabelle_C/src_ext/mlton/mlyacc/README

thys/Isabelle_C/src_ext/mlton/mlyacc/README.MLton

thys/Isabelle_C/src_ext/mlton/mlyacc/src/FILES

thys/Isabelle_C/src_ext/mlton/mlyacc/src/README

thys/Isabelle_C/src_ext/parser_menhir/LICENSE

thys/Isabelle_C/src_ext/parser_menhir/README.md

thys/Isabelle_C/src_ext/parser_menhir/tests/aligned_struct_c18.c

thys/Isabelle_C/src_ext/parser_menhir/tests/argument_scope.c

thys/Isabelle_C/src_ext/parser_menhir/tests/atomic.c

thys/Isabelle_C/src_ext/parser_menhir/tests/atomic_parenthesis.c

thys/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.c

thys/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.fail.c

thys/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.ok.c

thys/Isabelle_C/src_ext/parser_menhir/tests/block_scope.c

thys/Isabelle_C/src_ext/parser_menhir/tests/c-namespace.c

thys/Isabelle_C/src_ext/parser_menhir/tests/c11-noreturn.c

thys/Isabelle_C/src_ext/parser_menhir/tests/c1x-alignas.c

thys/Isabelle_C/src_ext/parser_menhir/tests/char-literal-printing.c

thys/Isabelle_C/src_ext/parser_menhir/tests/control-scope.c

thys/Isabelle_C/src_ext/parser_menhir/tests/dangling_else.c

thys/Isabelle_C/src_ext/parser_menhir/tests/dangling_else_lookahead.c

thys/Isabelle_C/src_ext/parser_menhir/tests/dangling_else_lookahead.if.c

thys/Isabelle_C/src_ext/parser_menhir/tests/dangling_else_misleading.fail.c

thys/Isabelle_C/src_ext/parser_menhir/tests/declaration_ambiguity.c

thys/Isabelle_C/src_ext/parser_menhir/tests/declarator_visibility.c

thys/Isabelle_C/src_ext/parser_menhir/tests/declarators.c

thys/Isabelle_C/src_ext/parser_menhir/tests/designator.c

thys/Isabelle_C/src_ext/parser_menhir/tests/enum-trick.c

thys/Isabelle_C/src_ext/parser_menhir/tests/enum.c

thys/Isabelle_C/src_ext/parser_menhir/tests/enum_constant_visibility.c

thys/Isabelle_C/src_ext/parser_menhir/tests/enum_shadows_typedef.c

thys/Isabelle_C/src_ext/parser_menhir/tests/expressions.c

thys/Isabelle_C/src_ext/parser_menhir/tests/function-decls.c

thys/Isabelle_C/src_ext/parser_menhir/tests/function_parameter_scope.c

thys/Isabelle_C/src_ext/parser_menhir/tests/function_parameter_scope_extends.c

thys/Isabelle_C/src_ext/parser_menhir/tests/if_scopes.c

thys/Isabelle_C/src_ext/parser_menhir/tests/local_scope.c

thys/Isabelle_C/src_ext/parser_menhir/tests/local_typedef.c

thys/Isabelle_C/src_ext/parser_menhir/tests/long-long-struct.c

thys/Isabelle_C/src_ext/parser_menhir/tests/loop_scopes.c

thys/Isabelle_C/src_ext/parser_menhir/tests/namespaces.c

thys/Isabelle_C/src_ext/parser_menhir/tests/no_local_scope.c

thys/Isabelle_C/src_ext/parser_menhir/tests/parameter_declaration_ambiguity.c

thys/Isabelle_C/src_ext/parser_menhir/tests/parameter_declaration_ambiguity.test.c

thys/Isabelle_C/src_ext/parser_menhir/tests/statements.c

thys/Isabelle_C/src_ext/parser_menhir/tests/struct-recursion.c

thys/Isabelle_C/src_ext/parser_menhir/tests/typedef_star.c

thys/Isabelle_C/src_ext/parser_menhir/tests/types.c

thys/Isabelle_C/src_ext/parser_menhir/tests/variable_star.c

thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy

thys/Poincare_Bendixson/Analysis_Misc.thy

thys/Poincare_Bendixson/Examples.thy

thys/Poincare_Bendixson/Invariance.thy

thys/Poincare_Bendixson/Limit_Set.thy

thys/Poincare_Bendixson/ODE_Misc.thy

thys/Poincare_Bendixson/Periodic_Orbit.thy

thys/Poincare_Bendixson/Poincare_Bendixson.thy

thys/Poincare_Bendixson/ROOT

thys/Poincare_Bendixson/document/root.tex

thys/ROOTS

web/entries/CISC-Kernel.html

web/entries/Circus.html

web/entries/Clean.html

web/entries/Featherweight_OCL.html

web/entries/Generalized_Counting_Sort.html

web/entries/HOL-CSP.html

web/entries/InfPathElimination.html

web/entries/Isabelle_C.html

web/entries/Isabelle_Meta_Model.html

web/entries/Ordinary_Differential_Equations.html

web/entries/Poincare_Bendixson.html

web/entries/TESL_Language.html

web/entries/UPF.html

web/entries/UPF_Firewall.html

web/entries/UTP.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html