Diffusion Isabelle 461ee3e49ad3

interpretation/interpret: prefixes are mandatory by default;
461ee3e49ad3
Actions

Tags

None

Subscribers

None

Description

interpretation/interpret: prefixes are mandatory by default;

Details

Provenance

Authored on

Parents

rISABELLEf0aeca99b5d9: interpretation/interpret: prefixes are mandatory by default;

Branches

Unknown

Tags

Unknown

Event Timeline

makarius mentioned this in rISABELLE1005c50b2750: prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as….Mar 21 2020, 10:18 PM

Changes (41)

Path

Size

doc-src/

Classes/

Thy/

document/

src/

FOL/

ex/

HOL/

Algebra/

Decision_Procs/

Dense_Linear_Order.thy

Groebner_Basis.thy

HahnBanach/

Library/

FrechetDeriv.thy

Inner_Product.thy

Numeral_Type.thy

Product_Vector.thy

SetsAndFunctions.thy

NSA/

Word/

WordBitwise.thy

WordDefinition.thy

ex/

LocaleTest2.thy

HOLCF/

CompactBasis.thy

ZF/

Constructible/

Rec_Separation.thy

rISABELLE461ee3e49ad3

doc-src/Classes/Thy/Classes.thy

Loading...

doc-src/Classes/Thy/document/Classes.tex

Loading...

src/FOL/ex/LocaleTest.thy

Loading...

src/HOL/Algebra/AbelCoset.thy

Loading...

src/HOL/Algebra/Group.thy

Loading...

src/HOL/Algebra/Ideal.thy

Loading...

src/HOL/Algebra/IntRing.thy

Loading...

src/HOL/Algebra/RingHom.thy

Loading...

src/HOL/Algebra/UnivPoly.thy

Loading...

src/HOL/Complex.thy

Loading...

src/HOL/Decision_Procs/Dense_Linear_Order.thy

Loading...

src/HOL/Divides.thy

Loading...

src/HOL/Finite_Set.thy

Loading...

src/HOL/Groebner_Basis.thy

Loading...

src/HOL/HahnBanach/Subspace.thy

Loading...

src/HOL/Lattices.thy

Loading...

src/HOL/Library/FrechetDeriv.thy

Loading...

src/HOL/Library/Inner_Product.thy

Loading...

src/HOL/Library/Multiset.thy

Loading...

src/HOL/Library/Numeral_Type.thy

Loading...

src/HOL/Library/Product_Vector.thy

Loading...

src/HOL/Library/SetsAndFunctions.thy

Loading...

src/HOL/NSA/StarDef.thy

Loading...

src/HOL/RealVector.thy

Loading...

src/HOL/Word/TdThs.thy

Loading...

src/HOL/Word/WordArith.thy

Loading...

src/HOL/Word/WordBitwise.thy

Loading...

src/HOL/Word/WordDefinition.thy

Loading...

src/HOL/Word/WordGenLib.thy

Loading...

src/HOL/ex/LocaleTest2.thy

Loading...

src/HOLCF/Algebraic.thy

Loading...

src/HOLCF/Bifinite.thy

Loading...

src/HOLCF/CompactBasis.thy

Loading...

src/HOLCF/Completion.thy

Loading...

src/HOLCF/ConvexPD.thy

Loading...

src/HOLCF/LowerPD.thy

Loading...

src/HOLCF/Universal.thy

Loading...

src/HOLCF/UpperPD.thy

Loading...

src/ZF/Constructible/L_axioms.thy

Loading...

src/ZF/Constructible/Rec_Separation.thy

Loading...

src/ZF/Constructible/Separation.thy

Loading...