# HG changeset patch # User wenzelm # Date 1126973485 -7200 # Node ID 93fc1211603f314798dedb16be6fd2b563bf39a6 # Parent a4090ccf14a8b71c5d076caefcd4100a07a47a22 removed obsolete BasisLibrary; diff -r a4090ccf14a8 -r 93fc1211603f TFL/tfl.ML --- 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; diff -r a4090ccf14a8 -r 93fc1211603f src/HOL/Integ/presburger.ML --- 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 diff -r a4090ccf14a8 -r 93fc1211603f src/HOL/MicroJava/BV/BVExample.thy --- 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") diff -r a4090ccf14a8 -r 93fc1211603f src/HOL/Tools/Presburger/presburger.ML --- 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 diff -r a4090ccf14a8 -r 93fc1211603f src/HOL/Tools/comm_ring.ML --- 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 diff -r a4090ccf14a8 -r 93fc1211603f src/HOL/ex/svc_funcs.ML --- 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; diff -r a4090ccf14a8 -r 93fc1211603f src/HOLCF/IOA/Modelcheck/MuIOA.ML --- 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) | diff -r a4090ccf14a8 -r 93fc1211603f src/HOLCF/domain/theorems.ML --- 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)) @