| author | Walther Neuper <walther.neuper@jku.at> |
| Fri, 10 Apr 2020 16:16:09 +0200 | |
| changeset 59867 | bb153a08645b |
| parent 59852 | ea7e6679080e |
| child 59879 | 33449c96d99f |
| permissions | -rw-r--r-- |
| neuper@48809 | 1 |
theory Lucas_Interpreter |
| wneuper@59592 | 2 |
imports Isac.Isac_Knowledge |
| neuper@48809 | 3 |
begin |
| neuper@48809 | 4 |
|
| neuper@48809 | 5 |
ML_file "lucas_interpreter.sml" |
| wneuper@59472 | 6 |
ML \<open> |
| walther@59867 | 7 |
(*val test_ruleset' = Unsynchronized.ref ([] : (Rule_Set.id * (theory' * rls)) list)*) |
| wneuper@59472 | 8 |
\<close> |
| neuper@48809 | 9 |
end |