clarified input and output: support markup blocks via Bg/En;
clarified datatype tree vs. tree_ops: reconstruct nested markup blocks via make_tree;
clarified tree_ops_ord: ignore markup blocks, proceed like dict_ord;
chapter FOL
session LCF = Pure +
description "
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
Logic for Computable Functions.
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
"
sessions
FOL
directories "ex"
theories
LCF
(* Some examples from Lawrence Paulson's book Logic and Computation *)
"ex/Ex1"
"ex/Ex2"
"ex/Ex3"
"ex/Ex4"