Diffusion afp-devel 9d50a3586261

removed Restricted_Predicates.total_on following the introduction of equivalent…
9d50a3586261
Actions

Tags

None

Subscribers

None

Description

removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL

Details

Provenance

Authored on

Parents

rAFP70cf7337c410: replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rAFP9d50a3586261: removed Restricted_Predicates.total_on following the introduction of equivalent….Oct 28 2022, 3:49 PM

Changes (4)

Path

Size

thys/

Open_Induction/

Restricted_Predicates.thy

PAC_Checker/

PAC_Checker.thy

PAC_Polynomials_Operations.thy

Well_Quasi_Orders/

Almost_Full.thy

rAFP9d50a3586261

thys/Open_Induction/Restricted_Predicates.thy

Loading...

thys/PAC_Checker/PAC_Checker.thy

Loading...

thys/PAC_Checker/PAC_Polynomials_Operations.thy

Loading...

thys/Well_Quasi_Orders/Almost_Full.thy

Loading...