--- a/src/HOL/Groebner_Basis.thy Wed May 05 16:46:18 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy Wed May 05 16:46:19 2010 +0200
@@ -7,7 +7,6 @@
theory Groebner_Basis
imports Numeral_Simprocs
uses
- "Tools/Groebner_Basis/misc.ML"
"Tools/Groebner_Basis/normalizer_data.ML"
("Tools/Groebner_Basis/normalizer.ML")
("Tools/Groebner_Basis/groebner.ML")
--- a/src/HOL/Tools/Groebner_Basis/misc.ML Wed May 05 16:46:18 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: HOL/Tools/Groebner_Basis/misc.ML
- ID: $Id$
- Author: Amine Chaieb, TU Muenchen
-
-Very basic stuff for cterms.
-*)
-
-structure Misc =
-struct
-
-fun is_comb ct =
- (case Thm.term_of ct of
- _ $ _ => true
- | _ => false);
-
-val concl = Thm.cprop_of #> Thm.dest_arg;
-
-fun is_binop ct ct' =
- (case Thm.term_of ct' of
- c $ _ $ _ => term_of ct aconv c
- | _ => false);
-
-fun dest_binop ct ct' =
- if is_binop ct ct' then Thm.dest_binop ct'
- else raise CTERM ("dest_binop: bad binop", [ct, ct'])
-
-fun inst_thm inst = Thm.instantiate ([], inst);
-
-end;