Now proof of Ord_jump_cardinal uses
ordertype_pred_unfold; proof of sum_0_eqpoll uses bij_0_sum; proof of
sum_0_eqpoll uses sum_prod_distrib_bij; proof of sum_assoc_eqpoll uses
sum_assoc_bij; proof of prod_assoc_eqpoll uses prod_assoc_bij. Proved
well_ord_cadd_cmult_distrib.
(* Title: Modal/ex/ROOT
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
Modal_build_completed; (*Cause examples to fail if Modal did*)
proof_timing := true;
writeln "\nTheorems of T\n";
fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
time_use "ex/Tthms.ML";
writeln "\nTheorems of S4\n";
fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
time_use "ex/Tthms.ML";
time_use "ex/S4thms.ML";
writeln "\nTheorems of S43\n";
fun try s = (writeln s;
prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE
S43_Prover.solve_tac 3]));
time_use "ex/Tthms.ML";
time_use "ex/S4thms.ML";
time_use "ex/S43thms.ML";
maketest"END: Root file for Modal examples";