| changeset 16417 | 9bc16273c2d4 |
| parent 14398 | c5c47703f763 |
| child 17589 | 58eeffd73be1 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 header {* Correctness of Definite Assignment *} |
1 header {* Correctness of Definite Assignment *} |
2 |
2 |
3 theory DefiniteAssignmentCorrect = WellForm + Eval: |
3 theory DefiniteAssignmentCorrect imports WellForm Eval begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc] |
6 Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc] |
7 *} |
7 *} |
8 |
8 |