equal
deleted
inserted
replaced
183 \<close> ML \<open> |
183 \<close> ML \<open> |
184 \<close> ML \<open> |
184 \<close> ML \<open> |
185 \<close> |
185 \<close> |
186 |
186 |
187 ML \<open> |
187 ML \<open> |
188 KEStore_Elems.set_ref_thy @{theory}; |
188 Know_Store.set_ref_thy @{theory}; |
189 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*); |
189 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*); |
190 \<close> |
190 \<close> |
191 |
191 |
192 section \<open>trials with Isabelle's functions\<close> |
192 section \<open>trials with Isabelle's functions\<close> |
193 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close> |
193 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close> |