simultaneous use_thys;
authorwenzelm
Tue Jul 31 23:23:28 2007 +0200 (2007-07-31)
changeset 24106f2965bf954dc
parent 24105 af364e2b4048
child 24107 fecafd71e758
simultaneous use_thys;
src/CCL/ROOT.ML
src/CCL/ex/ROOT.ML
src/CTT/ex/ROOT.ML
src/Cube/ROOT.ML
src/HOL/Auth/ROOT.ML
src/HOLCF/FOCUS/ROOT.ML
src/HOLCF/IMP/ROOT.ML
src/HOLCF/ex/ROOT.ML
src/LCF/ex/ROOT.ML
src/Sequents/LK/ROOT.ML
src/Sequents/ROOT.ML
     1.1 --- a/src/CCL/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     1.2 +++ b/src/CCL/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     1.3 @@ -6,13 +6,10 @@
     1.4  Classical Computational Logic based on First-Order Logic.
     1.5  *)
     1.6  
     1.7 -val banner = "Classical Computational Logic (in FOL)";
     1.8 -writeln banner;
     1.9 -
    1.10  set eta_contract;
    1.11  
    1.12  (* CCL - a computational logic for an untyped functional language *)
    1.13  (*                       with evaluation to weak head-normal form *)
    1.14  
    1.15 -use_thy "Wfd";
    1.16 -use_thy "Fix";
    1.17 +use_thys ["Wfd", "Fix"];
    1.18 +
     2.1 --- a/src/CCL/ex/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     2.2 +++ b/src/CCL/ex/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     2.3 @@ -6,7 +6,4 @@
     2.4  Examples for Classical Computational Logic.
     2.5  *)
     2.6  
     2.7 -time_use_thy "Nat";
     2.8 -time_use_thy "List";
     2.9 -time_use_thy "Stream";
    2.10 -time_use_thy "Flag";
    2.11 +use_thys ["Nat", "List", "Stream", "Flag"];
     3.1 --- a/src/CTT/ex/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     3.2 +++ b/src/CTT/ex/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     3.3 @@ -6,7 +6,4 @@
     3.4  Examples for Constructive Type Theory. 
     3.5  *)
     3.6  
     3.7 -use_thy "Typechecking";
     3.8 -use_thy "Elimination";
     3.9 -use_thy "Equality";
    3.10 -use_thy "Synthesis";
    3.11 +use_thys ["Typechecking", "Elimination", "Equality", "Synthesis"];
     4.1 --- a/src/Cube/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     4.2 +++ b/src/Cube/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     4.3 @@ -6,8 +6,4 @@
     4.4  The Lambda-Cube a la Barendregt.
     4.5  *)
     4.6  
     4.7 -val banner = "Barendregt's Lambda-Cube";
     4.8 -writeln banner;
     4.9 -
    4.10 -use_thy "Cube";
    4.11 -use_thy "Example";
    4.12 +use_thys ["Cube", "Example"];
     5.1 --- a/src/HOL/Auth/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     5.2 +++ b/src/HOL/Auth/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/Auth/ROOT
     5.5 +(*  Title:      HOL/Auth/ROOT.ML
     5.6      ID:         $Id$
     5.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8      Copyright   1996  University of Cambridge
     5.9 @@ -8,41 +8,46 @@
    5.10  
    5.11  no_document use_thy "NatPair";
    5.12  
    5.13 -set timing;
    5.14 +use_thys [
    5.15  
    5.16  (* Conventional protocols: rely on 
    5.17     conventional Message, Event and Public *)
    5.18  
    5.19  (*Shared-key protocols*)
    5.20 -time_use_thy "NS_Shared";
    5.21 -time_use_thy "Kerberos_BAN";
    5.22 -time_use_thy "Kerberos_BAN_Gets";
    5.23 -time_use_thy "KerberosIV";
    5.24 -time_use_thy "KerberosIV_Gets";
    5.25 -time_use_thy "KerberosV";
    5.26 -time_use_thy "OtwayRees";
    5.27 -time_use_thy "OtwayRees_AN";
    5.28 -time_use_thy "OtwayRees_Bad";
    5.29 -time_use_thy "OtwayReesBella";
    5.30 -time_use_thy "WooLam";
    5.31 -time_use_thy "Recur";
    5.32 -time_use_thy "Yahalom";
    5.33 -time_use_thy "Yahalom2";
    5.34 -time_use_thy "Yahalom_Bad";
    5.35 -time_use_thy "ZhouGollmann";
    5.36 +  "NS_Shared",
    5.37 +  "Kerberos_BAN",
    5.38 +  "Kerberos_BAN_Gets",
    5.39 +  "KerberosIV",
    5.40 +  "KerberosIV_Gets",
    5.41 +  "KerberosV",
    5.42 +  "OtwayRees",
    5.43 +  "OtwayRees_AN",
    5.44 +  "OtwayRees_Bad",
    5.45 +  "OtwayReesBella",
    5.46 +  "WooLam",
    5.47 +  "Recur",
    5.48 +  "Yahalom",
    5.49 +  "Yahalom2",
    5.50 +  "Yahalom_Bad",
    5.51 +  "ZhouGollmann",
    5.52  
    5.53  (*Public-key protocols*)
    5.54 -time_use_thy "NS_Public_Bad";
    5.55 -time_use_thy "NS_Public";
    5.56 -time_use_thy "TLS";
    5.57 -time_use_thy "CertifiedEmail";
    5.58 +  "NS_Public_Bad",
    5.59 +  "NS_Public",
    5.60 +  "TLS",
    5.61 +  "CertifiedEmail",
    5.62  
    5.63  (*Smartcard protocols: rely on conventional Message and on new
    5.64    EventSC and Smartcard *)
    5.65  
    5.66 -with_path "Smartcard" time_use_thy "ShoupRubin";
    5.67 -with_path "Smartcard" time_use_thy "ShoupRubinBella";
    5.68 +  "Smartcard/ShoupRubin",
    5.69 +  "Smartcard/ShoupRubinBella",
    5.70  
    5.71  (*Blanqui's "guard" concept: protocol-independent secrecy*)
    5.72 -with_path "Guard" (app time_use_thy)
    5.73 -  ["P1", "P2", "Guard_NS_Public", "Guard_OtwayRees", "Guard_Yahalom", "Proto"];
    5.74 +  "Guard/P1",
    5.75 +  "Guard/P2",
    5.76 +  "Guard/Guard_NS_Public",
    5.77 +  "Guard/Guard_OtwayRees",
    5.78 +  "Guard/Guard_Yahalom",
    5.79 +  "Guard/Proto"
    5.80 +];
     6.1 --- a/src/HOLCF/FOCUS/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     6.2 +++ b/src/HOLCF/FOCUS/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     6.3 @@ -6,9 +6,4 @@
     6.4  See README.html for further information.
     6.5  *)
     6.6  
     6.7 -val banner = "HOLCF/FOCUS";
     6.8 -writeln banner;
     6.9 -
    6.10 -with_path "~~/src/HOLCF/ex" use_thy "Fstreams";
    6.11 -use_thy "FOCUS";
    6.12 -use_thy "Buffer_adm";
    6.13 +use_thys ["Fstreams", "FOCUS", "Buffer_adm"];
     7.1 --- a/src/HOLCF/IMP/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     7.2 +++ b/src/HOLCF/IMP/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     7.3 @@ -4,6 +4,4 @@
     7.4      Copyright   1997  TU Muenchen
     7.5  *)
     7.6  
     7.7 -with_path "../../HOL/IMP" (no_document time_use_thy) "Natural";
     7.8 -time_use_thy "HoareEx";
     7.9 -
    7.10 +use_thys ["../../HOL/IMP/Natural", "HoareEx"];
     8.1 --- a/src/HOLCF/ex/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     8.2 +++ b/src/HOLCF/ex/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     8.3 @@ -4,11 +4,5 @@
     8.4  Misc HOLCF examples.
     8.5  *)
     8.6  
     8.7 -time_use_thy "Dnat";
     8.8 -time_use_thy "Stream";
     8.9 -time_use_thy "Dagstuhl";
    8.10 -time_use_thy "Focus_ex";
    8.11 -time_use_thy "Fix2";
    8.12 -time_use_thy "Hoare";
    8.13 -time_use_thy "Loop";
    8.14 -time_use_thy "Fixrec_ex";
    8.15 +use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
    8.16 +  "Loop", "Fixrec_ex"];
     9.1 --- a/src/LCF/ex/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     9.2 +++ b/src/LCF/ex/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     9.3 @@ -6,7 +6,4 @@
     9.4  Some examples from Lawrence Paulson's book Logic and Computation.
     9.5  *)
     9.6  
     9.7 -time_use_thy "Ex1";
     9.8 -time_use_thy "Ex2";
     9.9 -time_use_thy "Ex3";
    9.10 -time_use_thy "Ex4";
    9.11 +use_thys ["Ex1", "Ex2", "Ex3", "Ex4"];
    10.1 --- a/src/Sequents/LK/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
    10.2 +++ b/src/Sequents/LK/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
    10.3 @@ -6,7 +6,5 @@
    10.4  Examples for Classical Logic.
    10.5  *)
    10.6  
    10.7 -use_thy "Propositional";
    10.8 -use_thy "Quantifiers";
    10.9 -use_thy "Hard_Quantifiers";
   10.10 -use_thy "Nat";
   10.11 +use_thys ["Propositional", "Quantifiers", "Hard_Quantifiers", "Nat"];
   10.12 +
    11.1 --- a/src/Sequents/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
    11.2 +++ b/src/Sequents/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
    11.3 @@ -6,19 +6,7 @@
    11.4  Classical Sequent Calculus based on Pure Isabelle. 
    11.5  *)
    11.6  
    11.7 -val banner = "Sequent Calculii";
    11.8 -writeln banner;
    11.9 -
   11.10  Unify.trace_bound:= 20;
   11.11  Unify.search_bound := 40;
   11.12  
   11.13 -use_thy "LK";
   11.14 -
   11.15 -use_thy "ILL";
   11.16 -use_thy "ILL_predlog";
   11.17 -use_thy "Washing";
   11.18 -
   11.19 -use_thy "Modal0";
   11.20 -use_thy"T";
   11.21 -use_thy"S4";
   11.22 -use_thy"S43";
   11.23 +use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"];