Diffusion afp-devel a51281787c8b

merge of AFP 2020, fixed some proofs, but Relational_Disjoint_Set_Forests stays…
a51281787c8b
Actions

Tags

None

Subscribers

None

Description

merge of AFP 2020, fixed some proofs, but Relational_Disjoint_Set_Forests stays broken

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFP9c53d1265e3d: sitegen
rAFP821ca76f3c0d: sitegen for Saturation_Framework_Extensions (and also for five other entries)

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa51281787c8b: merge of AFP 2020, fixed some proofs, but Relational_Disjoint_Set_Forests stays….Aug 26 2020, 2:43 PM

Merged Changes

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

821ca76f3c0d sitegen for Saturation_Framework_Extensions (and also for five other entries)
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ac00f34583b0 new entry Saturation_Framework_Extensions
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a41d53bc4c69 a proof of concept for generic conversions
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a7b99e8a1d84 tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d4c56b2760cf reversing all the lex crap
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c47e491d6c30 merged
Author
paulson
Browse Repository
No Builds
No Audits
242c8f6d0ace more lex fixes, some tricky
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
7d42634829a4 removed double underscores + tuned comments
Author
blanchette
Browse Repository
No Builds
No Audits
52090471320f bring title of document in sync with title of entry
Author
blanchette
Browse Repository
No Builds
No Audits
d2a0a7ac2b78 fixing some lex problems
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
62b7aa536380 more lex fixes
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
fcf802f31002 some lex fixes
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
05908e2bd514 fixes for new-style definition of lexicographic ordering
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a067d7a7ff67 clarified signature (see Isabelle/2b41b710f6ef);
Author
makarius
Browse Repository
No Builds
No Audits
d31906039242 reduced redundancy by sharing theories with MFOTL_Monitor;
Author
Joshua Schneider <joshua.schneider@inf.ethz.ch>
Browse Repository
No Builds
No Audits
3c4396a19260 MFOTL_Monitor change history
Author
Joshua Schneider <joshua.schneider@inf.ethz.ch>
Browse Repository
No Builds
No Audits
b1639ed541b7 added abstract slicing framework to MFOTL_Monitor;
Author
Joshua Schneider <joshua.schneider@inf.ethz.ch>
Browse Repository
No Builds
No Audits
9a9bc053eb71 dedicated symbols for code generation, to pave way for generic conversions from…
Author
florian.haftmann
Browse Repository
No Builds
No Audits
7950cea20592 merged
Author
paulson
Browse Repository
No Builds
No Audits
633328cc6a47 more on order types
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
116a82414c28 dropped alias
Author
florian.haftmann
Browse Repository
No Builds
No Audits
3e79743d7844 separation of reversed bit lists from other material
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cac1c67360f3 further refinement of code equations for mask operation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f28d68deefa8 uniform mask operation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
52ddcd32c0c9 clearer separation of pre-word bit list material
Author
florian.haftmann
Browse Repository
No Builds
No Audits
9b629e0e6654 repaired document slip
Author
florian.haftmann
Browse Repository
No Builds
No Audits
ef3c8932106a more consequent transferability
Author
florian.haftmann
Browse Repository
No Builds
No Audits
40e16c534243 much faster proofs (cf. Isabelle/bad75618fb82);
Author
makarius
Browse Repository
No Builds
No Audits
7757456aafcf Fixed failing proofs.
Author
Achim D. Brucker <adbrucker@0x5f.org>
Browse Repository
No Builds
No Audits
34a339f71b38 Added proofs about get_tag_type.
Author
Achim D. Brucker <adbrucker@0x5f.org>
Browse Repository
No Builds
No Audits
226cc9fd1567 Mostly improving theory format (adding line breaks) and added
Author
Achim D. Brucker <adbrucker@0x5f.org>
Browse Repository
No Builds
No Audits
c02eaed866dc data extend is obsolete and should be identity;
Author
makarius
Browse Repository
No Builds
No Audits
8c7430699dc1 merge from afp-2020
Author
kleing
Browse Repository
No Builds
No Audits
ce2c72a0a05e concatentation of bit values
Author
florian.haftmann
Browse Repository
No Builds
No Audits
c99668f88e5f saturation framework: renamings
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
7b844df07b1c prefer canonically oriented lists of bits in definitions
Author
florian.haftmann
Browse Repository
No Builds
No Audits
1bb7b24f2cf5 more realistic timeout: 20min CPU time;
Author
makarius
Browse Repository
No Builds
No Audits
aeedb987222c tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
70ae335403b7 signed_take_bit
Author
florian.haftmann
Browse Repository
No Builds
No Audits
06640f317a79 Add new material, mostly centered around cartesian categories. Sync with my…
Author
"Eugene W. Stark <stark@cs.stonybrook.edu>"
Browse Repository
No Builds
No Audits
d04de3d51efb Fix failing proofs after update to Metis 2.4
Author
desharna
Browse Repository
No Builds
No Audits
1cdcce397e9d separation of traditional bit operations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a03e9b5d8dc9 factored out auxiliary theory
Author
florian.haftmann
Browse Repository
No Builds
No Audits
b5b8255ae4c4 more operations for maps
Author
Andreas Lochbihler
Browse Repository
No Builds
No Audits
f90f9d593a88 misc lemma tuning
Author
florian.haftmann
Browse Repository
No Builds
No Audits
81a8bf702c09 activated simproc defined_all
Author
florian.haftmann
Browse Repository
No Builds
No Audits
e0714a129570 updated documentation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
b8a6808299e5 obsolete duplicates
Author
florian.haftmann
Browse Repository
No Builds
No Audits
3ceb3fe8ab08 factored out ancient numeral representation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
82e10d1ca9e1 moved to Word_Lib
Author
florian.haftmann
Browse Repository
No Builds
No Audits

Changes (70)

Path

Size

metadata/

Amicable_Numbers

Amicable_Numbers.thy

Berlekamp_Zassenhaus/

Reconstruction.thy

Co_Snapshot.thy

Distributed_System.thy

LLL_Basis_Reduction/

LLL_Complexity.thy

LLL_Number_Bounds.thy

Ordinal_Partitions

Erdos_Milner.thy

Library_Additions.thy

Omega_Omega.thy

Relational_Disjoint_Set_Forests

Disjoint_Set_Forests.thy

Relational_Paths

More_Relation_Algebra.thy

Path_Algorithms.thy

Rooted_Paths.thy

Aggregation_Algebras.html

Amicable_Numbers.html

Chandy_Lamport.html

Nash_Williams.html

Ordered_Resolution_Prover.html

Ordinal_Partitions.html

Polynomial_Factorization.html

Pratt_Certificate.html

Relation_Algebra.html

Relational_Disjoint_Set_Forests.html

Relational_Paths.html

Stone_Kleene_Relation_Algebras.html

ZFC_in_HOL.html

statistics.html

rAFPa51281787c8b

metadata/metadata

Loading...

thys/Amicable_Numbers/Amicable_Numbers.thy

Loading...

thys/Amicable_Numbers/ROOT

Loading...

thys/Amicable_Numbers/document/root.bib

Loading...

thys/Amicable_Numbers/document/root.tex

Loading...

thys/Berlekamp_Zassenhaus/Poly_Mod.thy

Loading...

thys/Berlekamp_Zassenhaus/Reconstruction.thy

Loading...

thys/Chandy_Lamport/Co_Snapshot.thy

Loading...

thys/Chandy_Lamport/Distributed_System.thy

Loading...

thys/Chandy_Lamport/Example.thy

Loading...

thys/Chandy_Lamport/ROOT

Loading...

thys/Chandy_Lamport/Snapshot.thy

Loading...

thys/Chandy_Lamport/Swap.thy

Loading...

thys/Chandy_Lamport/Trace.thy

Loading...

thys/Chandy_Lamport/Util.thy

Loading...

thys/Chandy_Lamport/document/root.bib

Loading...

thys/Chandy_Lamport/document/root.tex

Loading...

thys/LLL_Basis_Reduction/LLL.thy

Loading...

thys/LLL_Basis_Reduction/LLL_Complexity.thy

Loading...

thys/LLL_Basis_Reduction/LLL_Impl.thy

Loading...

thys/LLL_Basis_Reduction/LLL_Number_Bounds.thy

Loading...

thys/Ordinal_Partitions/Erdos_Milner.thy

Loading...

thys/Ordinal_Partitions/Library_Additions.thy

Loading...

thys/Ordinal_Partitions/Omega_Omega.thy

Loading...

thys/Ordinal_Partitions/Partitions.thy

Loading...

thys/Ordinal_Partitions/ROOT

Loading...

thys/Ordinal_Partitions/document/root.bib

Loading...

thys/Ordinal_Partitions/document/root.tex

Loading...

thys/ROOTS

Loading...

thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy

Loading...

thys/Relational_Disjoint_Set_Forests/ROOT

Loading...

thys/Relational_Disjoint_Set_Forests/document/root.bib

Loading...

thys/Relational_Disjoint_Set_Forests/document/root.tex

Loading...

thys/Relational_Paths/More_Relation_Algebra.thy

Loading...

thys/Relational_Paths/Path_Algorithms.thy

Loading...

thys/Relational_Paths/Paths.thy

Loading...

thys/Relational_Paths/ROOT

Loading...

thys/Relational_Paths/Rooted_Paths.thy

Loading...

thys/Relational_Paths/document/root.bib

Loading...

thys/Relational_Paths/document/root.tex

Loading...

web/entries/Aggregation_Algebras.html

Loading...

web/entries/Amicable_Numbers.html

Loading...

web/entries/Chandy_Lamport.html

Loading...

web/entries/Nash_Williams.html

Loading...

web/entries/Ordered_Resolution_Prover.html

Loading...

web/entries/Ordinal_Partitions.html

Loading...

web/entries/Polynomial_Factorization.html

Loading...

web/entries/Pratt_Certificate.html

Loading...

web/entries/Relation_Algebra.html

Loading...

web/entries/Relational_Disjoint_Set_Forests.html

Loading...

web/entries/Relational_Paths.html

Loading...

web/entries/Stone_Kleene_Relation_Algebras.html

Loading...

web/entries/ZFC_in_HOL.html

Loading...

web/index.html

Loading...

web/rss.xml

Loading...

web/statistics.html

Loading...

web/topics.html

Loading...