Diffusion Isabelle 72631efa3821

explicitly reject 'handle' with catch-all patterns;
72631efa3821
Actions

Tags

None

Subscribers

None

Description

explicitly reject 'handle' with catch-all patterns;

Details

Provenance

Authored on

Parents

rISABELLE1b052426a2b7: avoid accidental 'handle' of interrupts;

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE72631efa3821: explicitly reject 'handle' with catch-all patterns;.Sep 28 2023, 8:07 PM

makarius mentioned this in rAFP9c5fe84ef108: adapted to Isabelle/72631efa3821;.Sep 29 2023, 2:04 PM

Changes (10)

Path

Size

src/

HOL/

Library/

Pure/

Isar/

ML/

ML_Bootstrap.thy

Tools/

rISABELLE72631efa3821

NEWS

Loading...

src/HOL/Library/code_test.ML

Loading...

src/HOL/Metis.thy

Loading...

src/Pure/Isar/attrib.ML

Loading...

src/Pure/ML/ml_compiler.ML

Loading...

src/Pure/ML/ml_context.ML

Loading...

src/Pure/ML/ml_file.ML

Loading...

src/Pure/ML_Bootstrap.thy

Loading...

src/Pure/Pure.thy

Loading...

src/Pure/Tools/debugger.ML

Loading...