--- 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" ****)
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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];
--- 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];
--- 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];
--- 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];
--- 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;
--- 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.*)
--- 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];
--- 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];
--- 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;
--- 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];
--- 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;
--- 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]
--- 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"
--- 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);
--- 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];
--- 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]);
--- 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))";
--- 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)
--- 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
***)
--- 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];
--- 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 =
--- 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));
--- 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);
--- 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))";
--- 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 \
--- 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