--- a/TFL/tfl.ML Sat Sep 17 18:11:24 2005 +0200
+++ b/TFL/tfl.ML Sat Sep 17 18:11:25 2005 +0200
@@ -45,8 +45,6 @@
val trace = ref false;
-open BasisLibrary;
-
structure R = Rules;
structure S = USyntax;
structure U = Utils;
--- a/src/HOL/Integ/presburger.ML Sat Sep 17 18:11:24 2005 +0200
+++ b/src/HOL/Integ/presburger.ML Sat Sep 17 18:11:25 2005 +0200
@@ -2,10 +2,12 @@
ID: $Id$
Author: Amine Chaieb and Stefan Berghofer, TU Muenchen
-Tactic for solving arithmetical Goals in Presburger Arithmetic
-*)
+Tactic for solving arithmetical Goals in Presburger Arithmetic.
-(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To enable this feature call the procedure with the parameter abs
+This version of presburger deals with occurences of functional symbols
+in the subgoal and abstract over them to try to prove the more general
+formula. It then resolves with the subgoal. To enable this feature
+call the procedure with the parameter abs.
*)
signature PRESBURGER =
@@ -237,7 +239,7 @@
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
let
- val g = BasisLibrary.List.nth (prems_of st, i - 1)
+ val g = List.nth (prems_of st, i - 1)
val sg = sign_of_thm st
(* The Abstraction step *)
val g' = if a then abstract_pres sg g else g
--- a/src/HOL/MicroJava/BV/BVExample.thy Sat Sep 17 18:11:24 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Sat Sep 17 18:11:25 2005 +0200
@@ -454,7 +454,7 @@
"op :" ("(_ mem _)")
"op Un" ("(_ union _)")
"image" ("map")
- "UNION" ("(fn A => fn f => BasisLibrary.List.concat (map f A))")
+ "UNION" ("(fn A => fn f => List.concat (map f A))")
"Bex" ("(fn A => fn f => exists f A)")
"Ball" ("(fn A => fn f => forall f A)")
"some_elem" ("hd")
--- a/src/HOL/Tools/Presburger/presburger.ML Sat Sep 17 18:11:24 2005 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Sat Sep 17 18:11:25 2005 +0200
@@ -2,10 +2,12 @@
ID: $Id$
Author: Amine Chaieb and Stefan Berghofer, TU Muenchen
-Tactic for solving arithmetical Goals in Presburger Arithmetic
-*)
+Tactic for solving arithmetical Goals in Presburger Arithmetic.
-(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To enable this feature call the procedure with the parameter abs
+This version of presburger deals with occurences of functional symbols
+in the subgoal and abstract over them to try to prove the more general
+formula. It then resolves with the subgoal. To enable this feature
+call the procedure with the parameter abs.
*)
signature PRESBURGER =
@@ -237,7 +239,7 @@
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
let
- val g = BasisLibrary.List.nth (prems_of st, i - 1)
+ val g = List.nth (prems_of st, i - 1)
val sg = sign_of_thm st
(* The Abstraction step *)
val g' = if a then abstract_pres sg g else g
--- a/src/HOL/Tools/comm_ring.ML Sat Sep 17 18:11:24 2005 +0200
+++ b/src/HOL/Tools/comm_ring.ML Sat Sep 17 18:11:25 2005 +0200
@@ -1,7 +1,8 @@
(* ID: $Id$
Author: Amine Chaieb
-Tactic for solving equalities over commutative rings *)
+Tactic for solving equalities over commutative rings.
+*)
signature COMM_RING =
sig
@@ -114,7 +115,7 @@
val norm_eq = thm "norm_eq"
fun comm_ring_tac i =(fn st =>
let
- val g = BasisLibrary.List.nth (prems_of st, i - 1)
+ val g = List.nth (prems_of st, i - 1)
val sg = sign_of_thm st
val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g)
val norm_eq_th = simplify cring_ss
--- a/src/HOL/ex/svc_funcs.ML Sat Sep 17 18:11:24 2005 +0200
+++ b/src/HOL/ex/svc_funcs.ML Sat Sep 17 18:11:25 2005 +0200
@@ -30,8 +30,6 @@
| Int of IntInf.int
| Rat of IntInf.int * IntInf.int;
- open BasisLibrary
-
fun signedInt i =
if i < 0 then "-" ^ IntInf.toString (~i)
else IntInf.toString i;
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Sat Sep 17 18:11:24 2005 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Sat Sep 17 18:11:25 2005 +0200
@@ -120,40 +120,40 @@
structured_tuple [] _ = raise malformed;
fun varlist_of _ _ [] = [] |
-varlist_of n s (a::r) = (s ^ (BasisLibrary.Int.toString(n))) :: (varlist_of (n+1) s r);
+varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r);
fun string_of [] = "" |
string_of (a::r) = a ^ " " ^ (string_of r);
fun tupel_typed_of _ _ _ [] = "" |
-tupel_typed_of sign s n [a] = s ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a |
+tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a |
tupel_typed_of sign s n (a::r) =
- s ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r);
+ s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r);
fun double_tupel_typed_of _ _ _ _ [] = "" |
double_tupel_typed_of sign s t n [a] =
- s ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a ^ "," ^
- t ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a |
+ s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
+ t ^ (Int.toString(n)) ^ "::" ^ a |
double_tupel_typed_of sign s t n (a::r) =
- s ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a ^ "," ^
- t ^ (BasisLibrary.Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
+ s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
+ t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
fun tupel_of _ _ _ [] = "" |
-tupel_of sign s n [a] = s ^ (BasisLibrary.Int.toString(n)) |
-tupel_of sign s n (a::r) = s ^ (BasisLibrary.Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
+tupel_of sign s n [a] = s ^ (Int.toString(n)) |
+tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
fun double_tupel_of _ _ _ _ [] = "" |
-double_tupel_of sign s t n [a] = s ^ (BasisLibrary.Int.toString(n)) ^ "," ^
- t ^ (BasisLibrary.Int.toString(n)) |
-double_tupel_of sign s t n (a::r) = s ^ (BasisLibrary.Int.toString(n)) ^ "," ^
- t ^ (BasisLibrary.Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
+double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^
+ t ^ (Int.toString(n)) |
+double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^
+ t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
fun eq_string _ _ _ [] = "" |
-eq_string s t n [a] = s ^ (BasisLibrary.Int.toString(n)) ^ " = " ^
- t ^ (BasisLibrary.Int.toString(n)) |
+eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^
+ t ^ (Int.toString(n)) |
eq_string s t n (a::r) =
- s ^ (BasisLibrary.Int.toString(n)) ^ " = " ^
- t ^ (BasisLibrary.Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
+ s ^ (Int.toString(n)) ^ " = " ^
+ t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
fun merge_var_and_type [] [] = "" |
merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) |
--- a/src/HOLCF/domain/theorems.ML Sat Sep 17 18:11:24 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Sat Sep 17 18:11:25 2005 +0200
@@ -269,7 +269,6 @@
if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
[eq1, eq2] end;
- open BasisLibrary (*restore original List*)
fun distincts [] = []
| distincts ((c,leqs)::cs) = List.concat
(ListPair.map (distinct c) ((map #1 cs),leqs)) @