Diffusion Isabelle ead56ad40e15

bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.
ead56ad40e15
Actions

Tags

None

Subscribers

None

Description

bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;

Details

Provenance

Authored on

Parents

rISABELLEa9b20bc32fa6: localized command 'syntax' and 'no_syntax';

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLEead56ad40e15: bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library..Sep 21 2021, 12:20 AM

makarius mentioned this in rAFPd12a1ce2753f: bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library..Sep 21 2021, 5:14 PM

Changes (12)

Path

Size

Doc/

Main/

Typeclass_Hierarchy/

Examples/

Knaster_Tarski.thy

Combine_PER.thy

Complete_Partial_Order2.thy

Lattice_Syntax.thy

rISABELLEead56ad40e15

src/Doc/Main/Main_Doc.thy

Loading...

src/Doc/Typeclass_Hierarchy/Setup.thy

Loading...

src/HOL/Examples/Knaster_Tarski.thy

Loading...

src/HOL/Library/Combine_PER.thy

Loading...

src/HOL/Library/Complete_Partial_Order2.thy

Loading...

src/HOL/Library/Lattice_Syntax.thy

Loading...

src/HOL/Library/Library.thy

Loading...

src/HOL/Library/Option_ord.thy

Loading...

src/HOL/Main.thy

Loading...