equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/Groebner_Basis/misc.ML |
|
2 ID: $Id$ |
|
3 Author: Amine Chaieb, TU Muenchen |
|
4 |
|
5 Very basic stuff for cterms. |
|
6 *) |
|
7 |
|
8 structure Misc = |
|
9 struct |
|
10 |
|
11 fun is_comb ct = |
|
12 (case Thm.term_of ct of |
|
13 _ $ _ => true |
|
14 | _ => false); |
|
15 |
|
16 val concl = Thm.cprop_of #> Thm.dest_arg; |
|
17 |
|
18 fun is_binop ct ct' = |
|
19 (case Thm.term_of ct' of |
|
20 c $ _ $ _ => term_of ct aconv c |
|
21 | _ => false); |
|
22 |
|
23 fun dest_binop ct ct' = |
|
24 if is_binop ct ct' then Thm.dest_binop ct' |
|
25 else raise CTERM ("dest_binop: bad binop", [ct, ct']) |
|
26 |
|
27 fun inst_thm inst = Thm.instantiate ([], inst); |
|
28 |
|
29 end; |
|