Removal of obsolete "open" commands from heads of .ML files
authorpaulson
Fri Jul 31 10:48:42 1998 +0200 (1998-07-31)
changeset 52234cb05273f764
parent 5222 3e40c6bffb87
child 5224 8d132a14e722
Removal of obsolete "open" commands from heads of .ML files
src/HOL/Auth/Event.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/IMP/Com.ML
src/HOL/IMP/Denotation.ML
src/HOL/IMP/Expr.ML
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Transition.ML
src/HOL/IMP/VC.ML
src/HOL/Induct/Acc.ML
src/HOL/Induct/Com.ML
src/HOL/Induct/Comb.ML
src/HOL/Induct/Exp.ML
src/HOL/Induct/LFilter.ML
src/HOL/Induct/Perm.ML
src/HOL/Induct/PropLog.ML
src/HOL/Induct/SList.ML
src/HOL/Induct/Simult.ML
src/HOL/Induct/Term.ML
     1.1 --- a/src/HOL/Auth/Event.ML	Thu Jul 30 23:14:41 1998 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Fri Jul 31 10:48:42 1998 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  Datatype of events; function "sees"; freshness
     1.5  *)
     1.6  
     1.7 -open Event;
     1.8 -
     1.9  AddIffs [Spy_in_bad, Server_not_bad];
    1.10  
    1.11  (**** Function "spies" ****)
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Thu Jul 30 23:14:41 1998 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Fri Jul 31 10:48:42 1998 +0200
     2.3 @@ -9,17 +9,11 @@
     2.4    Burrows, Abadi and Needham.  A Logic of Authentication.
     2.5    Proc. Royal Soc. 426 (1989)
     2.6  
     2.7 -Tidied by lcp.
     2.8 -*)
     2.9 -
    2.10 -open Kerberos_BAN;
    2.11 +  Confidentiality (secrecy) and authentication properties rely on 
    2.12 +  temporal checks: strong guarantees in a little abstracted - but
    2.13 +  very realistic - model (see .thy).
    2.14  
    2.15 -(*
    2.16 -   Confidentiality (secrecy) and authentication properties rely on 
    2.17 -   temporal checks: strong guarantees in a little abstracted - but
    2.18 -   very realistic - model (see .thy).
    2.19 -
    2.20 -   Total execution time: 158s
    2.21 +Tidied by lcp.
    2.22  *)
    2.23  
    2.24  proof_timing:=true;
     3.1 --- a/src/HOL/Auth/Message.ML	Thu Jul 30 23:14:41 1998 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Fri Jul 31 10:48:42 1998 +0200
     3.3 @@ -13,8 +13,6 @@
     3.4  by (Blast_tac 1);
     3.5  Addsimps [result()];
     3.6  
     3.7 -open Message;
     3.8 -
     3.9  AddIffs atomic.inject;
    3.10  AddIffs msg.inject;
    3.11  
     4.1 --- a/src/HOL/Auth/NS_Public.ML	Thu Jul 30 23:14:41 1998 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public.ML	Fri Jul 31 10:48:42 1998 +0200
     4.3 @@ -7,8 +7,6 @@
     4.4  Version incorporating Lowe's fix (inclusion of B's identify in round 2).
     4.5  *)
     4.6  
     4.7 -open NS_Public;
     4.8 -
     4.9  set proof_timing;
    4.10  HOL_quantifiers := false;
    4.11  
     5.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Jul 30 23:14:41 1998 +0200
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Jul 31 10:48:42 1998 +0200
     5.3 @@ -11,9 +11,6 @@
     5.4    Proc. Royal Soc. 426 (1989)
     5.5  *)
     5.6  
     5.7 -open NS_Public_Bad;
     5.8 -
     5.9 -set proof_timing;
    5.10  HOL_quantifiers := false;
    5.11  
    5.12  AddEs spies_partsEs;
     6.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Jul 30 23:14:41 1998 +0200
     6.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Jul 31 10:48:42 1998 +0200
     6.3 @@ -10,9 +10,6 @@
     6.4    Proc. Royal Soc. 426 (1989)
     6.5  *)
     6.6  
     6.7 -open NS_Shared;
     6.8 -
     6.9 -set proof_timing;
    6.10  HOL_quantifiers := false;
    6.11  
    6.12  AddEs spies_partsEs;
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jul 30 23:14:41 1998 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Jul 31 10:48:42 1998 +0200
     7.3 @@ -12,11 +12,6 @@
     7.4    Proc. Royal Soc. 426 (1989)
     7.5  *)
     7.6  
     7.7 -open OtwayRees;
     7.8 -
     7.9 -set proof_timing;
    7.10 -HOL_quantifiers := false;
    7.11 -
    7.12  AddEs spies_partsEs;
    7.13  AddDs [impOfSubs analz_subset_parts];
    7.14  AddDs [impOfSubs Fake_parts_insert];
     8.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jul 30 23:14:41 1998 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jul 31 10:48:42 1998 +0200
     8.3 @@ -12,11 +12,6 @@
     8.4    IEEE Trans. SE 22 (1), 1996
     8.5  *)
     8.6  
     8.7 -open OtwayRees_AN;
     8.8 -
     8.9 -set proof_timing;
    8.10 -HOL_quantifiers := false;
    8.11 -
    8.12  AddEs spies_partsEs;
    8.13  AddDs [impOfSubs analz_subset_parts];
    8.14  AddDs [impOfSubs Fake_parts_insert];
     9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jul 30 23:14:41 1998 +0200
     9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Jul 31 10:48:42 1998 +0200
     9.3 @@ -15,11 +15,6 @@
     9.4  indicates the possibility of this attack.
     9.5  *)
     9.6  
     9.7 -open OtwayRees_Bad;
     9.8 -
     9.9 -set proof_timing;
    9.10 -HOL_quantifiers := false;
    9.11 -
    9.12  AddEs spies_partsEs;
    9.13  AddDs [impOfSubs analz_subset_parts];
    9.14  AddDs [impOfSubs Fake_parts_insert];
    10.1 --- a/src/HOL/Auth/Public.ML	Thu Jul 30 23:14:41 1998 +0200
    10.2 +++ b/src/HOL/Auth/Public.ML	Fri Jul 31 10:48:42 1998 +0200
    10.3 @@ -8,9 +8,6 @@
    10.4  Server keys; initial states of agents; new nonces and keys; function "sees" 
    10.5  *)
    10.6  
    10.7 -
    10.8 -open Public;
    10.9 -
   10.10  (*** Basic properties of pubK & priK ***)
   10.11  
   10.12  AddIffs [inj_pubK RS inj_eq];
    11.1 --- a/src/HOL/Auth/Recur.ML	Thu Jul 30 23:14:41 1998 +0200
    11.2 +++ b/src/HOL/Auth/Recur.ML	Fri Jul 31 10:48:42 1998 +0200
    11.3 @@ -6,10 +6,6 @@
    11.4  Inductive relation "recur" for the Recursive Authentication protocol.
    11.5  *)
    11.6  
    11.7 -open Recur;
    11.8 -
    11.9 -set proof_timing;
   11.10 -HOL_quantifiers := false;
   11.11  Pretty.setdepth 30;
   11.12  
   11.13  
    12.1 --- a/src/HOL/Auth/Shared.ML	Thu Jul 30 23:14:41 1998 +0200
    12.2 +++ b/src/HOL/Auth/Shared.ML	Fri Jul 31 10:48:42 1998 +0200
    12.3 @@ -8,9 +8,6 @@
    12.4  Shared, long-term keys; initial states of agents
    12.5  *)
    12.6  
    12.7 -
    12.8 -open Shared;
    12.9 -
   12.10  (*** Basic properties of shrK ***)
   12.11  
   12.12  (*Injectiveness: Agents' long-term keys are distinct.*)
    13.1 --- a/src/HOL/Auth/TLS.ML	Thu Jul 30 23:14:41 1998 +0200
    13.2 +++ b/src/HOL/Auth/TLS.ML	Fri Jul 31 10:48:42 1998 +0200
    13.3 @@ -17,11 +17,6 @@
    13.4    rollback attacks).
    13.5  *)
    13.6  
    13.7 -open TLS;
    13.8 -
    13.9 -set proof_timing;
   13.10 -HOL_quantifiers := false;
   13.11 -
   13.12  (*Automatically unfold the definition of "certificate"*)
   13.13  Addsimps [certificate_def];
   13.14  
    14.1 --- a/src/HOL/Auth/WooLam.ML	Thu Jul 30 23:14:41 1998 +0200
    14.2 +++ b/src/HOL/Auth/WooLam.ML	Fri Jul 31 10:48:42 1998 +0200
    14.3 @@ -10,11 +10,6 @@
    14.4    IEEE Trans. S.E. 22(1), 1996, pages 6-15.
    14.5  *)
    14.6  
    14.7 -open WooLam;
    14.8 -
    14.9 -set proof_timing;
   14.10 -HOL_quantifiers := false;
   14.11 -
   14.12  AddEs spies_partsEs;
   14.13  AddDs [impOfSubs analz_subset_parts];
   14.14  AddDs [impOfSubs Fake_parts_insert];
    15.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jul 30 23:14:41 1998 +0200
    15.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jul 31 10:48:42 1998 +0200
    15.3 @@ -10,10 +10,6 @@
    15.4    Proc. Royal Soc. 426 (1989)
    15.5  *)
    15.6  
    15.7 -open Yahalom;
    15.8 -
    15.9 -set proof_timing;
   15.10 -HOL_quantifiers := false;
   15.11  Pretty.setdepth 25;
   15.12  
   15.13  
    16.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Jul 30 23:14:41 1998 +0200
    16.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Jul 31 10:48:42 1998 +0200
    16.3 @@ -12,11 +12,6 @@
    16.4    Proc. Royal Soc. 426 (1989)
    16.5  *)
    16.6  
    16.7 -open Yahalom2;
    16.8 -
    16.9 -set proof_timing;
   16.10 -HOL_quantifiers := false;
   16.11 -
   16.12  AddEs spies_partsEs;
   16.13  AddDs [impOfSubs analz_subset_parts];
   16.14  AddDs [impOfSubs Fake_parts_insert];
    17.1 --- a/src/HOL/IMP/Com.ML	Thu Jul 30 23:14:41 1998 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,7 +0,0 @@
    17.4 -(*  Title:      HOL/IMP/Com.ML
    17.5 -    ID:         $Id$
    17.6 -    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    17.7 -    Copyright   1994 TUM
    17.8 -*)
    17.9 -
   17.10 -open Com;
    18.1 --- a/src/HOL/IMP/Denotation.ML	Thu Jul 30 23:14:41 1998 +0200
    18.2 +++ b/src/HOL/IMP/Denotation.ML	Fri Jul 31 10:48:42 1998 +0200
    18.3 @@ -4,9 +4,6 @@
    18.4      Copyright   1994 TUM
    18.5  *)
    18.6  
    18.7 -open Denotation;
    18.8 -
    18.9 -
   18.10  (**** mono (Gamma(b,c)) ****)
   18.11  
   18.12  qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
    19.1 --- a/src/HOL/IMP/Expr.ML	Thu Jul 30 23:14:41 1998 +0200
    19.2 +++ b/src/HOL/IMP/Expr.ML	Fri Jul 31 10:48:42 1998 +0200
    19.3 @@ -7,8 +7,6 @@
    19.4  Not used in the rest of the language, but included for completeness.
    19.5  *)
    19.6  
    19.7 -open Expr;
    19.8 -
    19.9  val evala_elim_cases = map (evala.mk_cases aexp.simps)
   19.10     ["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i",
   19.11      "(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma)  -a-> i"
    20.1 --- a/src/HOL/IMP/Hoare.ML	Thu Jul 30 23:14:41 1998 +0200
    20.2 +++ b/src/HOL/IMP/Hoare.ML	Fri Jul 31 10:48:42 1998 +0200
    20.3 @@ -7,8 +7,6 @@
    20.4  wrt denotational semantics
    20.5  *)
    20.6  
    20.7 -open Hoare;
    20.8 -
    20.9  Goalw [hoare_valid_def] "|- {P}c{Q} ==> |= {P}c{Q}";
   20.10  by (etac hoare.induct 1);
   20.11      by (ALLGOALS Asm_simp_tac);
    21.1 --- a/src/HOL/IMP/Transition.ML	Thu Jul 30 23:14:41 1998 +0200
    21.2 +++ b/src/HOL/IMP/Transition.ML	Fri Jul 31 10:48:42 1998 +0200
    21.3 @@ -6,8 +6,6 @@
    21.4  Equivalence of Natural and Transition semantics
    21.5  *)
    21.6  
    21.7 -open Transition;
    21.8 -
    21.9  section "Winskel's Proof";
   21.10  
   21.11  AddSEs [rel_pow_0_E];
    22.1 --- a/src/HOL/IMP/VC.ML	Thu Jul 30 23:14:41 1998 +0200
    22.2 +++ b/src/HOL/IMP/VC.ML	Fri Jul 31 10:48:42 1998 +0200
    22.3 @@ -6,8 +6,6 @@
    22.4  Soundness and completeness of vc
    22.5  *)
    22.6  
    22.7 -open VC;
    22.8 -
    22.9  AddIs hoare.intrs;
   22.10  
   22.11  val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
    23.1 --- a/src/HOL/Induct/Acc.ML	Thu Jul 30 23:14:41 1998 +0200
    23.2 +++ b/src/HOL/Induct/Acc.ML	Fri Jul 31 10:48:42 1998 +0200
    23.3 @@ -9,8 +9,6 @@
    23.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    23.5  *)
    23.6  
    23.7 -open Acc;
    23.8 -
    23.9  (*The intended introduction rule*)
   23.10  val prems = goal Acc.thy
   23.11      "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
   23.12 @@ -46,25 +44,25 @@
   23.13  qed "acc_induct";
   23.14  
   23.15  
   23.16 -val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
   23.17 -by (rtac (major RS wfI) 1);
   23.18 +Goal "r <= (acc r) Times (acc r) ==> wf(r)";
   23.19 +by (etac wfI 1);
   23.20  by (etac acc.induct 1);
   23.21  by (rewtac pred_def);
   23.22  by (Fast_tac 1);
   23.23  qed "acc_wfI";
   23.24  
   23.25 -val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
   23.26 -by (rtac (major RS wf_induct) 1);
   23.27 +Goal "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
   23.28 +by (etac wf_induct 1);
   23.29  by (rtac (impI RS allI) 1);
   23.30  by (rtac accI 1);
   23.31  by (Fast_tac 1);
   23.32  qed "acc_wfD_lemma";
   23.33  
   23.34 -val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
   23.35 +Goal "wf(r) ==> r <= (acc r) Times (acc r)";
   23.36  by (rtac subsetI 1);
   23.37  by (res_inst_tac [("p", "x")] PairE 1);
   23.38  by (fast_tac (claset() addSIs [SigmaI,
   23.39 -                             major RS acc_wfD_lemma RS spec RS mp]) 1);
   23.40 +			       acc_wfD_lemma RS spec RS mp]) 1);
   23.41  qed "acc_wfD";
   23.42  
   23.43  Goal "wf(r)  =  (r <= (acc r) Times (acc r))";
    24.1 --- a/src/HOL/Induct/Com.ML	Thu Jul 30 23:14:41 1998 +0200
    24.2 +++ b/src/HOL/Induct/Com.ML	Fri Jul 31 10:48:42 1998 +0200
    24.3 @@ -6,8 +6,6 @@
    24.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
    24.5  *)
    24.6  
    24.7 -open Com;
    24.8 -
    24.9  AddIs exec.intrs;
   24.10  
   24.11  val exec_elim_cases = map (exec.mk_cases exp.simps)
    25.1 --- a/src/HOL/Induct/Comb.ML	Thu Jul 30 23:14:41 1998 +0200
    25.2 +++ b/src/HOL/Induct/Comb.ML	Fri Jul 31 10:48:42 1998 +0200
    25.3 @@ -15,8 +15,6 @@
    25.4  /usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
    25.5  *)
    25.6  
    25.7 -open Comb;
    25.8 -
    25.9  (*** Reflexive/Transitive closure preserves the Church-Rosser property 
   25.10       So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
   25.11  ***)
    26.1 --- a/src/HOL/Induct/Exp.ML	Thu Jul 30 23:14:41 1998 +0200
    26.2 +++ b/src/HOL/Induct/Exp.ML	Fri Jul 31 10:48:42 1998 +0200
    26.3 @@ -6,8 +6,6 @@
    26.4  Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
    26.5  *)
    26.6  
    26.7 -open Exp;
    26.8 -
    26.9  AddSIs [eval.N, eval.X];
   26.10  AddIs  [eval.Op, eval.valOf];
   26.11  
    27.1 --- a/src/HOL/Induct/LFilter.ML	Thu Jul 30 23:14:41 1998 +0200
    27.2 +++ b/src/HOL/Induct/LFilter.ML	Fri Jul 31 10:48:42 1998 +0200
    27.3 @@ -7,9 +7,6 @@
    27.4    --defined by a combination of induction and coinduction
    27.5  *)
    27.6  
    27.7 -open LFilter;
    27.8 -
    27.9 -
   27.10  (*** findRel: basic laws ****)
   27.11  
   27.12  val findRel_LConsE = 
    28.1 --- a/src/HOL/Induct/Perm.ML	Thu Jul 30 23:14:41 1998 +0200
    28.2 +++ b/src/HOL/Induct/Perm.ML	Fri Jul 31 10:48:42 1998 +0200
    28.3 @@ -11,8 +11,6 @@
    28.4  See mset on HOL/ex/Sorting.thy
    28.5  *)
    28.6  
    28.7 -open Perm;
    28.8 -
    28.9  Goal "l <~~> l";
   28.10  by (induct_tac "l" 1);
   28.11  by (REPEAT (ares_tac perm.intrs 1));
    29.1 --- a/src/HOL/Induct/PropLog.ML	Thu Jul 30 23:14:41 1998 +0200
    29.2 +++ b/src/HOL/Induct/PropLog.ML	Fri Jul 31 10:48:42 1998 +0200
    29.3 @@ -8,8 +8,6 @@
    29.4  Prove: If H|=p then G|=p where G:Fin(H)
    29.5  *)
    29.6  
    29.7 -open PropLog;
    29.8 -
    29.9  (** Monotonicity **)
   29.10  Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
   29.11  by (rtac lfp_mono 1);
    30.1 --- a/src/HOL/Induct/SList.ML	Thu Jul 30 23:14:41 1998 +0200
    30.2 +++ b/src/HOL/Induct/SList.ML	Fri Jul 31 10:48:42 1998 +0200
    30.3 @@ -6,8 +6,6 @@
    30.4  Definition of type 'a list by a least fixed point
    30.5  *)
    30.6  
    30.7 -open SList;
    30.8 -
    30.9  val list_con_defs = [NIL_def, CONS_def];
   30.10  
   30.11  Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
    31.1 --- a/src/HOL/Induct/Simult.ML	Thu Jul 30 23:14:41 1998 +0200
    31.2 +++ b/src/HOL/Induct/Simult.ML	Fri Jul 31 10:48:42 1998 +0200
    31.3 @@ -11,8 +11,6 @@
    31.4  file may be superior for other simultaneous recursions.
    31.5  *)
    31.6  
    31.7 -open Simult;
    31.8 -
    31.9  (*** Monotonicity and unfolding of the function ***)
   31.10  
   31.11  Goal "mono(%Z.  A <*> Part Z In1 \
    32.1 --- a/src/HOL/Induct/Term.ML	Thu Jul 30 23:14:41 1998 +0200
    32.2 +++ b/src/HOL/Induct/Term.ML	Fri Jul 31 10:48:42 1998 +0200
    32.3 @@ -7,9 +7,7 @@
    32.4    (essentially the same type as in Trees & Forests)
    32.5  *)
    32.6  
    32.7 -open Term;
    32.8 -
    32.9 -(*** Monotonicity and unfolding of the function ***)
   32.10 +(** Monotonicity and unfolding of the function **)
   32.11  
   32.12  Goal "term(A) = A <*> list(term(A))";
   32.13  by (fast_tac (claset() addSIs term.intrs