src/Tools/isac/Specify/i-model.sml
changeset 60708 9e987411cfda
parent 60706 632abf0c253c
child 60710 21ae85b023bb
     1.1 --- a/src/Tools/isac/Specify/i-model.sml	Wed Apr 05 17:46:25 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Sat Apr 29 15:53:37 2023 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  
     1.5    type T
     1.6    type T_TEST
     1.7 +  val OLD_to_TEST: T -> T_TEST
     1.8    val empty: T
     1.9    val empty_TEST: T_TEST
    1.10    type single
    1.11 @@ -33,6 +34,7 @@
    1.12    val single_to_string_TEST: Proof.context -> single_TEST -> string
    1.13    val to_string: Proof.context -> T -> string
    1.14    val to_string_TEST: Proof.context -> T_TEST -> string
    1.15 +  val feedback_OLD_to_TEST: feedback -> feedback_TEST
    1.16  
    1.17    datatype add_single = Add of single | Err of string
    1.18    val init: Model_Pattern.T -> T