Lars,Thanks for the information about PROP. I experimented with it some, but I couldn't figure out how to use it with "abbreviation" to not get an error.
All the typing looks right for this: abbreviation (input) tester :: "prop ⇒ prop" where "tester x == x" term "tester (A ==> B)" (* "A::bool ==> B::bool" :: "prop" *) --"1" theorem "PROP tester (A ⟹ B)" oops theorem "tester (A ==> B)" (* Error *)Using PROP to turn off all the coercion like with --"1" is not the thing to do.
It typed "sequ1233a (A ==> B)" just fine (note again, A, B :: bool, surrounded by a Tr)). However, another Tr is applied to "sequ1233a (A ==> B)" which then cannot be typed.
Somehow getting around "another Tr is applied to "sequ1233a (A ==> B)" is the problem. The ==> operator requires I give it a prop, and the automatic Trueprop requires the abbreviation return it a bool. I can make my abbreviation "'a => 'a", "prop => prop", and "bool => prop", but I can't make it "prop => bool".
I've improvised some to get more mileage out of what I have.Trueprop priority is 5, and ==> priority is 1, so I only have priorities 1, 2, 3, and 4 to use for other notation for ==>. I put the turnstile at priority 4, and cycle the use of priorities 1, 2, and 3 with other operators, so I don't have to use parentheses. When I go from 3 to 4, I have to use parentheses, but 4, 5, and 6 operators can be parentheses free in their block.
I attached a screen shot. Getting everything to line up is big. Six levels should be enough for most things.
Description: PNG image