| changeset 13208 | 965f95a3abd9 |
| parent 12486 | 0ed8bdd883e0 |
| child 14981 | e73f8140af78 |
| 13207:0d07e49dc9a5 | 13208:965f95a3abd9 |
|---|---|
1 (* Title: HOL/Prolog/Func.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 open Func; |
7 open Func; |
2 |
8 |
3 val prog_Func = prog_HOHH @ [eval]; |
9 val prog_Func = prog_HOHH @ [eval]; |
4 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func)); |
10 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func)); |
5 val p = ptac prog_Func 1; |
11 val p = ptac prog_Func 1; |