Diffusion Isabelle 033f90dc441d

redefined wf as an abbreviation for "wf_on UNIV"
033f90dc441d
Actions

Tags

None

Subscribers

None

Description

redefined wf as an abbreviation for "wf_on UNIV"

Details

Provenance

Authored on

Parents

rISABELLEf83e9e9a898e: tuned NEWS

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rISABELLE033f90dc441d: redefined wf as an abbreviation for "wf_on UNIV".Mar 23 2024, 6:55 PM

desharna mentioned this in rAFPecd2bddb6e88: adapted to new definition of wf following Isabelle/033f90dc441d.Mar 25 2024, 10:24 AM

Changes (11)

Path

Size

src/

HOL/

Library/

Tools/

Function/

induction_schema.ML

Nitpick/

Nunchaku/

nunchaku_collect.ML

Wellfounded.thy

rISABELLE033f90dc441d

NEWS

Loading...

src/HOL/Library/Multiset.thy

Loading...

src/HOL/Library/RBT_Set.thy

Loading...

src/HOL/Library/old_recdef.ML

Loading...

src/HOL/List.thy

Loading...

src/HOL/Nitpick.thy

Loading...

src/HOL/Tools/Function/induction_schema.ML

Loading...

src/HOL/Tools/Function/termination.ML

Loading...

src/HOL/Tools/Nitpick/nitpick_hol.ML

Loading...

src/HOL/Tools/Nunchaku/nunchaku_collect.ML

Loading...

src/HOL/Wellfounded.thy

Loading...