author | lcp |
Tue, 21 Jun 1994 17:20:34 +0200 | |
changeset 435 | ca5356bd315a |
parent 393 | 02b27671b899 |
child 1297 | 7ac266cf82d0 |
permissions | -rw-r--r-- |
(* Title: LK/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. Should be executed in the subdirectory LK. *) val banner = "Classical First-Order Sequent Calculus"; writeln banner; init_thy_reader(); print_depth 1; use_thy "LK"; use "../Pure/install_pp.ML"; print_depth 8; val LK_build_completed = (); (*indicate successful build*)