added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
(* Title: HOLCF/sprod1.thy
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
Partial ordering for the strict product.
*)
Sprod1 = Sprod0 +
instance "**"::(sq_ord,sq_ord)sq_ord
defs
less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
end