9000
|
1 |
(* Title: CTT/ex/ROOT.ML
|
1459
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
0
|
3 |
Copyright 1991 University of Cambridge
|
|
4 |
|
19761
|
5 |
Examples for Constructive Type Theory.
|
0
|
6 |
*)
|
|
7 |
|
24106
|
8 |
use_thys ["Typechecking", "Elimination", "Equality", "Synthesis"];
|