author | paulson |
Wed, 07 Oct 1998 10:31:30 +0200 | |
changeset 5619 | 76a8c72e3fd4 |
parent 5210 | 54aaa779b6b4 |
child 6349 | f7750d816c21 |
permissions | -rw-r--r-- |
(* Title: Sequents/ROOT ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Adds Classical Sequent Calculus to a database containing pure Isabelle. *) val banner = "Sequent Calculii"; writeln banner; print_depth 1; use_thy "Sequents"; use "prover.ML"; use_thy "LK"; use_thy "ILL"; use_thy "Modal0"; use_thy"T"; use_thy"S4"; use_thy"S43"; print_depth 8; val Sequents_build_completed = (); (*indicate successful build*)