equal
deleted
inserted
replaced
13 type single = Model_Def.o_model_single |
13 type single = Model_Def.o_model_single |
14 type variants = Model_Def.variants |
14 type variants = Model_Def.variants |
15 type m_field = Model_Def.m_field |
15 type m_field = Model_Def.m_field |
16 type descriptor = Model_Def.descriptor |
16 type descriptor = Model_Def.descriptor |
17 val to_string: T -> string |
17 val to_string: T -> string |
|
18 val single_to_string: single -> string |
18 val single_empty: single |
19 val single_empty: single |
19 |
20 |
20 val init: Formalise.model -> theory -> Model_Pattern.T -> T |
21 val init: Formalise.model -> theory -> Model_Pattern.T -> T |
21 (*val add_method: theory -> Model_Pattern.T -> T ..TODO*) |
22 (*val add_method: theory -> Model_Pattern.T -> T ..TODO*) |
22 |
23 |
44 type descriptor = Model_Def.descriptor; |
45 type descriptor = Model_Def.descriptor; |
45 |
46 |
46 type T = Model_Def.o_model; |
47 type T = Model_Def.o_model; |
47 type single = Model_Def.o_model_single |
48 type single = Model_Def.o_model_single |
48 val single_empty = Model_Def.o_model_empty; |
49 val single_empty = Model_Def.o_model_empty; |
|
50 val single_to_string = Model_Def.o_model_single_to_string; |
49 val to_string = Model_Def.o_model_to_string; |
51 val to_string = Model_Def.o_model_to_string; |
50 |
52 |
51 (* O_Model.single without leading integer *) |
53 (* O_Model.single without leading integer *) |
52 type preori = (variants * m_field * term * term list); |
54 type preori = (variants * m_field * term * term list); |
53 fun preori2str (vs, fi, t, ts) = |
55 fun preori2str (vs, fi, t, ts) = |