We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 50e4b8e commit 9358a27Copy full SHA for 9358a27
src/lite/liteLib.sml
@@ -454,10 +454,8 @@ fun MK_FORALL v th =
454
let val theta = [{redex=Type.alpha, residue=Term.type_of v}]
455
in AP_TERM (Term.inst theta boolSyntax.universal) (ABS v th)
456
end;
457
-fun MK_EXISTS v th =
458
- let val theta = [{redex=Type.alpha, residue=Term.type_of v}]
459
- in AP_TERM (Term.inst theta boolSyntax.existential) (ABS v th)
460
- end;
+
+val MK_EXISTS = Drule.MK_EXISTS
461
462
fun SIMPLE_DISJ_CASES th1 th2 =
463
case (hyp th1, hyp th2)
0 commit comments