Re: [isabelle] Trying to fit HOL to traditional math verbiage

The function type operator (the "=>" we were using
before) is primitive, that is, not created by type definition. In the
usual model of HOL in set theory, it constructs function spaces.

Makes sense, I guess. And even in src/ZF/ZF.thy I see that primitive.

It's all functional programming. That's my revelation of yesterday. Anything that gives me recursion is probably going to be functional programming.

My requirements have changed. All I want is the easiest possible way to learn a tool that allows me to do some logic and have the appearance of sets. If there's a problem, it's false illusions.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.