equal
deleted
inserted
replaced
11 ML_file contextC.sml |
11 ML_file contextC.sml |
12 ML_file environment.sml |
12 ML_file environment.sml |
13 |
13 |
14 ML \<open> |
14 ML \<open> |
15 \<close> ML \<open> |
15 \<close> ML \<open> |
16 \<close> ML \<open> |
16 \<close> text \<open> |
|
17 fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = dest_numeral' t |
|
18 (* |
|
19 | string_of_atom (t as Const ("Groups.one_class.one", _)) = HOLogic.dest_numeral t |
|
20 | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = HOLogic.dest_numeral t |
|
21 | string_of_atom (Const (str, _)) = str |
|
22 | string_of_atom (Free _) = true |
|
23 | string_of_atom (Var _) = true |
|
24 | string_of_atom _ = false; |
|
25 *) |
17 \<close> ML \<open> |
26 \<close> ML \<open> |
18 \<close> ML \<open> |
27 \<close> ML \<open> |
19 \<close> ML \<open> |
28 \<close> ML \<open> |
20 \<close> ML \<open> |
29 \<close> ML \<open> |
21 \<close> ML \<open> |
30 \<close> ML \<open> |