--- a/src/ZF/ex/Prop.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Prop.ML Fri Jul 01 11:04:12 1994 +0200
@@ -12,13 +12,10 @@
(val thy = Univ.thy;
val rec_specs =
[("prop", "univ(0)",
- [(["Fls"], "i"),
- (["Var"], "i=>i"),
- (["op =>"], "[i,i]=>i")])];
+ [(["Fls"], "i",NoSyn),
+ (["Var"], "i=>i", Mixfix ("#_", [100], 100)),
+ (["=>"], "[i,i]=>i", Infixr 90)])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext
- [OldMixfix.Mixfix("#_", "i => i", "Var", [100], 100),
- OldMixfix.Infixr("=>", "[i,i] => i", 90)]);
val sintrs =
["Fls : prop",
"n: nat ==> #n : prop",