| author | Walther Neuper <walther.neuper@jku.at> |
| Wed, 08 Apr 2020 12:32:51 +0200 | |
| changeset 59852 | ea7e6679080e |
| parent 59592 | 99c8d2ff63eb |
| child 59867 | bb153a08645b |
| 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@59852 | 7 |
(*val test_ruleset' = Unsynchronized.ref ([] : (Rule_Set.identifier * (theory' * rls)) list)*) |
| wneuper@59472 | 8 |
\<close> |
| neuper@48809 | 9 |
end |