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