--- a/src/ZF/ex/prop.ML Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/prop.ML Thu Sep 30 10:54:01 1993 +0100
@@ -16,19 +16,9 @@
(["Var"], "i=>i"),
(["op =>"], "[i,i]=>i")])];
val rec_styp = "i";
- val ext = Some (NewSext {
- mixfix =
- [Mixfix("#_", "i => i", "Var", [100], 100),
- Infixr("=>", "[i,i] => i", 90)],
- xrules = [],
- parse_ast_translation = [],
- parse_preproc = None,
- parse_postproc = None,
- parse_translation = [],
- print_translation = [],
- print_preproc = None,
- print_postproc = None,
- print_ast_translation = []});
+ val ext = Some (Syntax.simple_sext
+ [Mixfix("#_", "i => i", "Var", [100], 100),
+ Infixr("=>", "[i,i] => i", 90)]);
val sintrs =
["Fls : prop",
"n: nat ==> #n : prop",