# Landau's "Grundlagen der Analysis", formal specification in AUTOMATH
# Copyright (C) 1977, L.S. van Benthem Jutting
# 1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
# Landau's "Grundlagen der Analysis", formal specification in AUTOMATH
# Copyright (C) 1977, L.S. van Benthem Jutting
# 1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b)
-iff
@[sigma:'type'][p:[x:sigma]'prop']
thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b)
-iff
@[sigma:'type'][p:[x:sigma]'prop']