# HG changeset patch
# User paulson
# Date 901874922 -7200
# Node ID 4cb05273f7641880b44a52454e80734a250acbb5
# Parent  3e40c6bffb877ba946c0c5cb1aa25c00078ad010
Removal of obsolete "open" commands from heads of .ML files

diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Event.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -8,8 +8,6 @@
 Datatype of events; function "sees"; freshness
 *)
 
-open Event;
-
 AddIffs [Spy_in_bad, Server_not_bad];
 
 (**** Function "spies" ****)
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -9,17 +9,11 @@
   Burrows, Abadi and Needham.  A Logic of Authentication.
   Proc. Royal Soc. 426 (1989)
 
-Tidied by lcp.
-*)
-
-open Kerberos_BAN;
+  Confidentiality (secrecy) and authentication properties rely on 
+  temporal checks: strong guarantees in a little abstracted - but
+  very realistic - model (see .thy).
 
-(*
-   Confidentiality (secrecy) and authentication properties rely on 
-   temporal checks: strong guarantees in a little abstracted - but
-   very realistic - model (see .thy).
-
-   Total execution time: 158s
+Tidied by lcp.
 *)
 
 proof_timing:=true;
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -13,8 +13,6 @@
 by (Blast_tac 1);
 Addsimps [result()];
 
-open Message;
-
 AddIffs atomic.inject;
 AddIffs msg.inject;
 
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -7,8 +7,6 @@
 Version incorporating Lowe's fix (inclusion of B's identify in round 2).
 *)
 
-open NS_Public;
-
 set proof_timing;
 HOL_quantifiers := false;
 
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -11,9 +11,6 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-open NS_Public_Bad;
-
-set proof_timing;
 HOL_quantifiers := false;
 
 AddEs spies_partsEs;
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -10,9 +10,6 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-open NS_Shared;
-
-set proof_timing;
 HOL_quantifiers := false;
 
 AddEs spies_partsEs;
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -12,11 +12,6 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-open OtwayRees;
-
-set proof_timing;
-HOL_quantifiers := false;
-
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -12,11 +12,6 @@
   IEEE Trans. SE 22 (1), 1996
 *)
 
-open OtwayRees_AN;
-
-set proof_timing;
-HOL_quantifiers := false;
-
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -15,11 +15,6 @@
 indicates the possibility of this attack.
 *)
 
-open OtwayRees_Bad;
-
-set proof_timing;
-HOL_quantifiers := false;
-
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Public.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -8,9 +8,6 @@
 Server keys; initial states of agents; new nonces and keys; function "sees" 
 *)
 
-
-open Public;
-
 (*** Basic properties of pubK & priK ***)
 
 AddIffs [inj_pubK RS inj_eq];
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Recur.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -6,10 +6,6 @@
 Inductive relation "recur" for the Recursive Authentication protocol.
 *)
 
-open Recur;
-
-set proof_timing;
-HOL_quantifiers := false;
 Pretty.setdepth 30;
 
 
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -8,9 +8,6 @@
 Shared, long-term keys; initial states of agents
 *)
 
-
-open Shared;
-
 (*** Basic properties of shrK ***)
 
 (*Injectiveness: Agents' long-term keys are distinct.*)
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/TLS.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -17,11 +17,6 @@
   rollback attacks).
 *)
 
-open TLS;
-
-set proof_timing;
-HOL_quantifiers := false;
-
 (*Automatically unfold the definition of "certificate"*)
 Addsimps [certificate_def];
 
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/WooLam.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -10,11 +10,6 @@
   IEEE Trans. S.E. 22(1), 1996, pages 6-15.
 *)
 
-open WooLam;
-
-set proof_timing;
-HOL_quantifiers := false;
-
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -10,10 +10,6 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-open Yahalom;
-
-set proof_timing;
-HOL_quantifiers := false;
 Pretty.setdepth 25;
 
 
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -12,11 +12,6 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-open Yahalom2;
-
-set proof_timing;
-HOL_quantifiers := false;
-
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/IMP/Com.ML
--- a/src/HOL/IMP/Com.ML	Thu Jul 30 23:14:41 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      HOL/IMP/Com.ML
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-open Com;
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/IMP/Denotation.ML
--- a/src/HOL/IMP/Denotation.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/IMP/Denotation.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -4,9 +4,6 @@
     Copyright   1994 TUM
 *)
 
-open Denotation;
-
-
 (**** mono (Gamma(b,c)) ****)
 
 qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/IMP/Expr.ML
--- a/src/HOL/IMP/Expr.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/IMP/Expr.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -7,8 +7,6 @@
 Not used in the rest of the language, but included for completeness.
 *)
 
-open Expr;
-
 val evala_elim_cases = map (evala.mk_cases aexp.simps)
    ["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i",
     "(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma)  -a-> i"
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/IMP/Hoare.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -7,8 +7,6 @@
 wrt denotational semantics
 *)
 
-open Hoare;
-
 Goalw [hoare_valid_def] "|- {P}c{Q} ==> |= {P}c{Q}";
 by (etac hoare.induct 1);
     by (ALLGOALS Asm_simp_tac);
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/IMP/Transition.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -6,8 +6,6 @@
 Equivalence of Natural and Transition semantics
 *)
 
-open Transition;
-
 section "Winskel's Proof";
 
 AddSEs [rel_pow_0_E];
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/IMP/VC.ML
--- a/src/HOL/IMP/VC.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/IMP/VC.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -6,8 +6,6 @@
 Soundness and completeness of vc
 *)
 
-open VC;
-
 AddIs hoare.intrs;
 
 val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -9,8 +9,6 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-open Acc;
-
 (*The intended introduction rule*)
 val prems = goal Acc.thy
     "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
@@ -46,25 +44,25 @@
 qed "acc_induct";
 
 
-val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
-by (rtac (major RS wfI) 1);
+Goal "r <= (acc r) Times (acc r) ==> wf(r)";
+by (etac wfI 1);
 by (etac acc.induct 1);
 by (rewtac pred_def);
 by (Fast_tac 1);
 qed "acc_wfI";
 
-val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
-by (rtac (major RS wf_induct) 1);
+Goal "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
+by (etac wf_induct 1);
 by (rtac (impI RS allI) 1);
 by (rtac accI 1);
 by (Fast_tac 1);
 qed "acc_wfD_lemma";
 
-val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
+Goal "wf(r) ==> r <= (acc r) Times (acc r)";
 by (rtac subsetI 1);
 by (res_inst_tac [("p", "x")] PairE 1);
 by (fast_tac (claset() addSIs [SigmaI,
-                             major RS acc_wfD_lemma RS spec RS mp]) 1);
+			       acc_wfD_lemma RS spec RS mp]) 1);
 qed "acc_wfD";
 
 Goal "wf(r)  =  (r <= (acc r) Times (acc r))";
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Com.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -6,8 +6,6 @@
 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
 *)
 
-open Com;
-
 AddIs exec.intrs;
 
 val exec_elim_cases = map (exec.mk_cases exp.simps)
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Comb.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -15,8 +15,6 @@
 /usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
 *)
 
-open Comb;
-
 (*** Reflexive/Transitive closure preserves the Church-Rosser property 
      So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
 ***)
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Exp.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -6,8 +6,6 @@
 Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
 *)
 
-open Exp;
-
 AddSIs [eval.N, eval.X];
 AddIs  [eval.Op, eval.valOf];
 
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/LFilter.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -7,9 +7,6 @@
   --defined by a combination of induction and coinduction
 *)
 
-open LFilter;
-
-
 (*** findRel: basic laws ****)
 
 val findRel_LConsE = 
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Perm.ML
--- a/src/HOL/Induct/Perm.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Perm.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -11,8 +11,6 @@
 See mset on HOL/ex/Sorting.thy
 *)
 
-open Perm;
-
 Goal "l <~~> l";
 by (induct_tac "l" 1);
 by (REPEAT (ares_tac perm.intrs 1));
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/PropLog.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -8,8 +8,6 @@
 Prove: If H|=p then G|=p where G:Fin(H)
 *)
 
-open PropLog;
-
 (** Monotonicity **)
 Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
 by (rtac lfp_mono 1);
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/SList.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -6,8 +6,6 @@
 Definition of type 'a list by a least fixed point
 *)
 
-open SList;
-
 val list_con_defs = [NIL_def, CONS_def];
 
 Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Simult.ML
--- a/src/HOL/Induct/Simult.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Simult.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -11,8 +11,6 @@
 file may be superior for other simultaneous recursions.
 *)
 
-open Simult;
-
 (*** Monotonicity and unfolding of the function ***)
 
 Goal "mono(%Z.  A <*> Part Z In1 \
diff -r 3e40c6bffb87 -r 4cb05273f764 src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/Term.ML	Fri Jul 31 10:48:42 1998 +0200
@@ -7,9 +7,7 @@
   (essentially the same type as in Trees & Forests)
 *)
 
-open Term;
-
-(*** Monotonicity and unfolding of the function ***)
+(** Monotonicity and unfolding of the function **)
 
 Goal "term(A) = A <*> list(term(A))";
 by (fast_tac (claset() addSIs term.intrs