equal
deleted
inserted
replaced
|
1 (* Title: HOL/Prolog/Type.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 *) |
|
6 |
1 val prog_Type = prog_Func @ [good_typeof,common_typeof]; |
7 val prog_Type = prog_Func @ [good_typeof,common_typeof]; |
2 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type)); |
8 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type)); |
3 val p = ptac prog_Type 1; |
9 val p = ptac prog_Type 1; |
4 |
10 |
5 pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"; |
11 pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"; |