equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1997 University of Cambridge |
4 Copyright 1997 University of Cambridge |
5 |
5 |
6 Example of Mutual Induction via Iteratived Inductive Definitions: Expressions |
6 Example of Mutual Induction via Iteratived Inductive Definitions: Expressions |
7 *) |
7 *) |
8 |
|
9 open Exp; |
|
10 |
8 |
11 AddSIs [eval.N, eval.X]; |
9 AddSIs [eval.N, eval.X]; |
12 AddIs [eval.Op, eval.valOf]; |
10 AddIs [eval.Op, eval.valOf]; |
13 |
11 |
14 val eval_elim_cases = map (eval.mk_cases exp.simps) |
12 val eval_elim_cases = map (eval.mk_cases exp.simps) |