blob: b547a89b9358139b4d84da2a7995571103528216 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
type mlarg =
Mlint of int
| Mlstring of string
| Mlterm of term
| Mltype of hol_type
| Mlthm of mldata
| Mlpair of mlarg * mlarg
| Mllist of mlarg list
| Mlfn of mldata
and mldata = string * mlarg list;; (* ML object name and args *)
type label =
Tactical of mldata
| Label of string;;
(* Atomic tests *)
let is_atomic_mlarg arg =
match arg with
Mlthm (_,(_::_)) | Mlpair _ | Mlfn (_, _::_) -> false
| _ -> true;;
let is_atomic_mldata ((x,args):mldata) = (is_empty args);;
(* active_info *)
let active_info = ("...",[]);;
|
