--- 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)
--------------------------------
--- 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);
--- 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";
--- 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
--- 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);
--- 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";
--- 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";
--- 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";
--- 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";
--- 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