equal
deleted
inserted
replaced
1107 Parse}. For running the ML-interpreter we need the following |
1107 Parse}. For running the ML-interpreter we need the following |
1108 scaffolding code. |
1108 scaffolding code. |
1109 *} |
1109 *} |
1110 |
1110 |
1111 ML %grayML{* |
1111 ML %grayML{* |
1112 structure Result = |
1112 structure Result = Proof_Data |
1113 Proof_Data (type T = unit -> term |
1113 (type T = unit -> term |
1114 fun init thy () = error "Result") |
1114 fun init thy () = error "Result") |
1115 |
1115 |
1116 val result_cookie = (Result.get, Result.put, "Result.put") *} |
1116 val result_cookie = (Result.get, Result.put, "Result.put") *} |
1117 |
1117 |
1118 text {* |
1118 text {* |
1119 With this in place, we can implement the code for \isacommand{foobar\_prove} |
1119 With this in place, we can implement the code for \isacommand{foobar\_prove} |