equal
deleted
inserted
replaced
1 (* Title: Tools/Compute_Oracle/linker.ML |
1 (* Title: HOL/Matrix/Compute_Oracle/linker.ML |
2 Author: Steven Obua |
2 Author: Steven Obua |
3 |
3 |
4 This module solves the problem that the computing oracle does not |
4 This module solves the problem that the computing oracle does not |
5 instantiate polymorphic rules. By going through the PCompute |
5 instantiate polymorphic rules. By going through the PCompute |
6 interface, all possible instantiations are resolved by compiling new |
6 interface, all possible instantiations are resolved by compiling new |