1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Sep 10 10:47:18 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Sep 10 16:13:28 2019 +0200
     1.3 @@ -65,11 +65,13 @@
     1.4    and "IsacScripts" is determined in KEStore.thy.
     1.5  \<close>
     1.6  ML \<open>
     1.7 -val thydata_list = 
     1.8 +val thydata_list = []
     1.9 +(*//--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------\\* )
    1.10    collect_part       "IsacKnowledge" knowledge_parent knowthys' @
    1.11    (map (collect_isab "Isabelle") rlsthmsNOTisac) @
    1.12    collect_part       "IsacScripts" proglang_parent progthys'
    1.13  : (Celem.theID * Celem.thydata) list
    1.14 +( *\\--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------//*)
    1.15  \<close>
    1.16  setup \<open>KEStore_Elems.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
    1.17  
    1.18 @@ -89,6 +91,7 @@
    1.19            @{thm  diff_exp_chain}])]]
    1.20  \<close>
    1.21  
    1.22 +(*//--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------\* )
    1.23  setup \<open>
    1.24  KEStore_Elems.insert_fillpats
    1.25    [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
    1.26 @@ -104,6 +107,7 @@
    1.27        TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Celem.fillpat list))
    1.28    ]
    1.29  \<close>
    1.30 +( *\\--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------//*)
    1.31  
    1.32  subsubsection \<open>Error patterns for calculation with rationals\<close>
    1.33