# HG changeset patch
# User paulson
# Date 1077211448 -3600
# Node ID 477380c74c1d2b8f8e5db4e9793147170b29d593
# Parent  6069098854b9e869ee4307d744d401797549085d
removal of the legacy ML structure List

diff -r 6069098854b9 -r 477380c74c1d NEWS
--- a/NEWS	Thu Feb 19 17:57:54 2004 +0100
+++ b/NEWS	Thu Feb 19 18:24:08 2004 +0100
@@ -101,7 +101,7 @@
   - INCOMPATIBILITY: many type-specific instances of laws proved in 
     Ring_and_Field are no longer available.
 
-* Type "rat" of the rational numbers is now availabe in HOL-Complex.
+* Type "rat" of the rational numbers is now available in HOL-Complex.
 
 * Records:
   - Record types are now by default printed with their type abbreviation
@@ -119,8 +119,6 @@
 
 * HOL-Algebra: new locale "ring" for non-commutative rings.
 
-* SET-Protocol: formalization and verification of the SET protocol suite;
-
 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
  defintions, thanks to Sava Krsti\'{c} and John Matthews.
 
@@ -131,6 +129,8 @@
   Similarly for "\<Union>x. B", and for \<Inter> instead of \<Union>.
   The subscript version is also accepted as input syntax.
 
+* ML: the legacy theory structures Int and List have been removed. They had
+  conflicted with ML Basis Library structures having the same names.
 
 New in Isabelle2003 (May 2003)
 --------------------------------
diff -r 6069098854b9 -r 477380c74c1d src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOL/Lex/MaxChop.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -80,7 +80,7 @@
                         addsplits [split_split]) 1);
 by (Clarify_tac 1);
 by (rename_tac "xs1 ys1 xss1 ys" 1);
-by (split_asm_tac [list.split_asm] 1);
+by (split_asm_tac [thm "list.split_asm"] 1);
  by (Asm_full_simp_tac 1);
  by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
  by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
diff -r 6069098854b9 -r 477380c74c1d src/HOL/Lex/RegExp2NA.ML
--- a/src/HOL/Lex/RegExp2NA.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -249,7 +249,7 @@
 Goalw [conc_def]
  "!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | \
 \                          (? s. p = False#s & fin R s))";
-by (simp_tac (simpset() addsplits [list.split]) 1);
+by (simp_tac (simpset() addsplits [thm"list.split"]) 1);
 by (Blast_tac 1);
 qed_spec_mp "final_conc";
 
diff -r 6069098854b9 -r 477380c74c1d src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -408,7 +408,7 @@
 
 Goalw [conc_def]
  "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
-by (simp_tac (simpset() addsplits [list.split]) 1);
+by (simp_tac (simpset() addsplits [thm"list.split"]) 1);
 qed_spec_mp "final_conc";
 
 Goal
diff -r 6069098854b9 -r 477380c74c1d src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -135,7 +135,7 @@
  "!i j xs. xs : regset d i j k = \
 \          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
 by (induct_tac "k" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [list.split]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong] addsplits [thm"list.split"]) 1);
 by (strip_tac 1);
 by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
 by (rtac iffI 1);
diff -r 6069098854b9 -r 477380c74c1d src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOL/List.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -1,40 +1,6 @@
 
 (** legacy ML bindings **)
 
-structure List =
-struct
-
-val thy = the_context ();
-
-structure list =
-struct
-  val distinct = thms "list.distinct";
-  val inject = thms "list.inject";
-  val exhaust = thm "list.exhaust";
-  val cases = thms "list.cases";
-  val split = thm "list.split";
-  val split_asm = thm "list.split_asm";
-  val induct = thm "list.induct";
-  val recs = thms "list.recs";
-  val simps = thms "list.simps";
-  val size = thms "list.size";
-end;
-
-structure lists =
-struct
-  val intrs = thms "lists.intros";
-  val elims = thms "lists.cases";
-  val elim = thm "lists.cases";
-  val induct = thm "lists.induct";
-  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "List.lists";
-  val [Nil, Cons] = intrs;
-end;
-
-end;
-
-open List;
-
-
 val Cons_eq_appendI = thm "Cons_eq_appendI";
 val Cons_in_lex = thm "Cons_in_lex";
 val Nil2_notin_lex = thm "Nil2_notin_lex";
diff -r 6069098854b9 -r 477380c74c1d src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOL/MiniML/Type.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -373,7 +373,7 @@
 Addsimps [bound_tv_subst_scheme];
 
 Goal "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
-by (rtac list.induct 1);
+by (rtac (thm"list.induct") 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "bound_tv_subst_scheme_list";
@@ -627,7 +627,7 @@
 Addsimps [subst_TVar_scheme];
 
 Goal "!!A::type_scheme list. $ TVar A = A";
-by (rtac list.induct 1);
+by (rtac (thm"list.induct") 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list])));
 qed "subst_TVar_scheme_list";
 
diff -r 6069098854b9 -r 477380c74c1d src/HOLCF/IOA/ABP/Correctness.ML
--- a/src/HOLCF/IOA/ABP/Correctness.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -41,26 +41,26 @@
 
 Goal "(reduce(l)=[]) = (l=[])";  
 by (induct_tac "l" 1);
-by (auto_tac (claset(), simpset() addsplits [list.split]));
+by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
 val l_iff_red_nil = result();
 
 Goal "s~=[] --> hd(s)=hd(reduce(s))";
 by (induct_tac "s" 1);
-by (auto_tac (claset(), simpset() addsplits [list.split]));
+by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
 qed"hd_is_reduce_hd";
 
 (* to be used in the following Lemma *)
 Goal "l~=[] --> reverse(reduce(l))~=[]";
 by (induct_tac "l" 1);
-by (auto_tac (claset(), simpset() addsplits [list.split]));
+by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
 qed_spec_mp "rev_red_not_nil";
 
 (* shows applicability of the induction hypothesis of the following Lemma 1 *)
 Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
  by (Simp_tac 1);
- by (asm_full_simp_tac (list_ss addsplits [list.split]
+ by (auto_tac (claset(), HOL_ss addsplits [thm"list.split"]
                                 addsimps [reverse_Cons,hd_append,
-					  rev_red_not_nil])  1);
+					  rev_red_not_nil]));
 qed"last_ind_on_first";
 
 val impl_ss = simpset() delsimps [reduce_Cons];
@@ -106,7 +106,7 @@
 by (cut_inst_tac [("l","s")] cons_not_nil 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT (etac exE 1));
-by (auto_tac (claset(), simpset() addsplits [list.split]));
+by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
 val reduce_tl =result();
 
 
@@ -145,12 +145,12 @@
 Addsplits [split_if]; 
 
 Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
-by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
+by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
  srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
 qed"sender_abstraction";
 
 Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
-by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
+by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
  srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
 qed"receiver_abstraction";
 
diff -r 6069098854b9 -r 477380c74c1d src/HOLCF/IOA/ABP/Lemmas.ML
--- a/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -37,16 +37,14 @@
 
 (* Lists *)
 
-val list_ss = simpset_of List.thy;
-
-goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
+Goal "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
 by (induct_tac "l" 1);
-by (simp_tac list_ss 1);
-by (simp_tac list_ss 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
 val hd_append =result();
 
-goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
+Goal "l ~= [] --> (? x xs. l = (x#xs))";
  by (induct_tac "l" 1);
- by (simp_tac list_ss 1);
+ by (Simp_tac 1);
  by (Fast_tac 1);
 qed"cons_not_nil";
diff -r 6069098854b9 -r 477380c74c1d src/HOLCF/IOA/ABP/Lemmas.thy
--- a/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Feb 19 18:24:08 2004 +0100
@@ -6,4 +6,4 @@
 Arithmetic lemmas.
 *)
 
-Lemmas = NatArith
+Lemmas = Main