changeset 283 | 76caebd18756 |
parent 0 | a5a9c433f639 |
--- a/src/LK/lk.thy Thu Mar 17 13:54:50 1994 +0100 +++ b/src/LK/lk.thy Thu Mar 17 17:48:37 1994 +0100 @@ -7,11 +7,17 @@ *) LK = Pure + + classes term < logic + default term -types o 0 - sequence,seqobj,seqcont,sequ,sobj 0 -arities o :: logic + +types + o sequence seqobj seqcont sequ sobj + +arities + o :: logic + consts True,False :: "o" "=" :: "['a,'a] => o" (infixl 50)