new Close_locale synatx
authorpaulson
Fri Dec 11 10:41:53 1998 +0100 (1998-12-11)
changeset 6024cb87f103d114
parent 6023 832b9269dedd
child 6025 f0e244e2123c
new Close_locale synatx
src/HOL/Finite.ML
src/HOL/Induct/Multiset.ML
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/UNITY/Lift.ML
src/HOL/ex/LocaleGroup.ML
     1.1 --- a/src/HOL/Finite.ML	Fri Dec 11 10:38:51 1998 +0100
     1.2 +++ b/src/HOL/Finite.ML	Fri Dec 11 10:41:53 1998 +0100
     1.3 @@ -675,7 +675,7 @@
     1.4  Delrules [empty_foldSetE];
     1.5  Delrules foldSet.intrs;
     1.6  
     1.7 -Close_locale();
     1.8 +Close_locale "LC";
     1.9  
    1.10  Open_locale "ACe"; 
    1.11  
    1.12 @@ -722,7 +722,7 @@
    1.13             [export fold_insert,insert_absorb, Int_insert_left]) 1);
    1.14  qed "fold_Un_disjoint2";
    1.15  
    1.16 -Close_locale();
    1.17 +Close_locale "ACe";
    1.18  
    1.19  Delrules ([empty_foldSetE] @ foldSet.intrs);
    1.20  Delsimps [foldSet_imp_finite];
     2.1 --- a/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:38:51 1998 +0100
     2.2 +++ b/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:41:53 1998 +0100
     2.3 @@ -431,7 +431,7 @@
     2.4  by(blast_tac (claset() addDs [export lemma3]) 1);
     2.5  qed "all_accessible";
     2.6  
     2.7 -Close_locale();
     2.8 +Close_locale "MSOrd";
     2.9  
    2.10  Goal "wf(r) ==> wf(mult1 r)";
    2.11  by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
     3.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Fri Dec 11 10:38:51 1998 +0100
     3.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Fri Dec 11 10:41:53 1998 +0100
     3.3 @@ -552,6 +552,6 @@
     3.4  
     3.5  val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
     3.6  
     3.7 -Close_locale();
     3.8 +Close_locale "UFT";
     3.9  
    3.10  
     4.1 --- a/src/HOL/UNITY/Lift.ML	Fri Dec 11 10:38:51 1998 +0100
     4.2 +++ b/src/HOL/UNITY/Lift.ML	Fri Dec 11 10:41:53 1998 +0100
     4.3 @@ -435,4 +435,4 @@
     4.4  by (Blast_tac 1);
     4.5  qed "lift_1";
     4.6  
     4.7 -Close_locale();
     4.8 +Close_locale "floor";
     5.1 --- a/src/HOL/ex/LocaleGroup.ML	Fri Dec 11 10:38:51 1998 +0100
     5.2 +++ b/src/HOL/ex/LocaleGroup.ML	Fri Dec 11 10:41:53 1998 +0100
     5.3 @@ -139,7 +139,7 @@
     5.4  by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
     5.5  qed "right_cancellation";
     5.6  
     5.7 -Close_locale();
     5.8 +Close_locale "groups";
     5.9  
    5.10  (* example what happens if export *)
    5.11  val Left_cancellation = export left_cancellation;