src/HOL/ex/While_Combinator_Example.thy
changeset 73014 90f4df1970b8
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
73013:d4b67dc6f4eb 73014:90f4df1970b8