equal
deleted
inserted
replaced
393 thy; |
393 thy; |
394 |
394 |
395 |
395 |
396 (** Pure setup **) |
396 (** Pure setup **) |
397 |
397 |
398 val _ = Context.add_setup |
398 val _ = Context.>> |
399 (add_types [("prop", ([], NONE))] #> |
399 (add_types [("prop", ([], NONE))] #> |
400 |
400 |
401 add_typeof_eqns |
401 add_typeof_eqns |
402 ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ |
402 ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ |
403 \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ |
403 \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ |