# HG changeset patch # User clasohm # Date 751293315 -3600 # Node ID 099d949fe46778aaf8d4747786cfd64393a0a644 # Parent 729fe026c5f35576e5cb75a2f036d4cc438c10cd changes for new Readthy diff -r 729fe026c5f3 -r 099d949fe467 src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/CCL/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -11,7 +11,7 @@ (* Higher-Order Set Theory Extension to FOL *) (* used as basis for CCL *) -(*set_load_path [".", "../FOL"]; wait for new Readthy*) +set_loadpath [".", "../FOL"]; use_thy "set"; use "subset.ML"; diff -r 729fe026c5f3 -r 099d949fe467 src/CTT/ROOT.ML --- a/src/CTT/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/CTT/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -12,6 +12,9 @@ print_depth 1; +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); +open Readthy; + use_thy"ctt"; use "../Provers/typedsimp.ML"; use "rew.ML"; diff -r 729fe026c5f3 -r 099d949fe467 src/Cube/ROOT.ML --- a/src/Cube/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/Cube/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -9,6 +9,9 @@ val banner = "Barendregt's Lambda-Cube"; writeln banner; +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); +open Readthy; + print_depth 1; use_thy "cube"; diff -r 729fe026c5f3 -r 099d949fe467 src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/FOL/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -11,6 +11,9 @@ writeln banner; +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); +open Readthy; + print_depth 1; use_thy "ifol"; use_thy "fol"; diff -r 729fe026c5f3 -r 099d949fe467 src/FOLP/ROOT.ML --- a/src/FOLP/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/FOLP/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -12,6 +12,9 @@ writeln banner; +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); +open Readthy; + print_depth 1; use_thy "ifolp"; use_thy "folp"; diff -r 729fe026c5f3 -r 099d949fe467 src/LCF/ROOT.ML --- a/src/LCF/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/LCF/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -11,6 +11,8 @@ val banner = "Logic for Computable Functions (in FOL)"; writeln banner; +set_loadpath [".", "../FOL"]; + print_depth 1; use_thy "lcf"; use"simpdata.ML"; diff -r 729fe026c5f3 -r 099d949fe467 src/LK/ROOT.ML --- a/src/LK/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/LK/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -10,6 +10,9 @@ val banner = "Classical First-Order Sequent Calculus"; writeln banner; +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); +open Readthy; + print_depth 1; use_thy "lk"; diff -r 729fe026c5f3 -r 099d949fe467 src/Modal/ROOT.ML --- a/src/Modal/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/Modal/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -7,6 +7,8 @@ val banner = "Modal Logic (over LK)"; writeln banner; +set_loadpath [".", "../LK"]; + use_thy "modal0"; structure Modal0_rls =