1.1 --- a/src/Tools/isac/KEStore.thy	Thu Jun 05 08:53:54 2014 +0200
     1.2 +++ b/src/Tools/isac/KEStore.thy	Thu Jun 05 09:09:53 2014 +0200
     1.3 @@ -170,6 +170,15 @@
     1.4  thehier := insrt theID2 thydata2 theID2 (get_thes ());
     1.5  thehier := insrt theID3 thydata3 theID3 (get_thes ());
     1.6  *}
     1.7 +setup {* (* determine sequence of main parts in thehier *)
     1.8 +KEStore_Elems.add_thes
     1.9 +  [(Html {guh = part2guh ["IsacKnowledge"], html = "",
    1.10 +    mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
    1.11 +  (Html {guh = part2guh ["Isabelle"], html = "",
    1.12 +    mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
    1.13 +  (Html {guh = part2guh ["IsacScripts"], html = "",
    1.14 +    mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
    1.15 +*}
    1.16  
    1.17  section {* Functions for checking KEStore_Elems *}
    1.18  ML {*

     2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Jun 05 08:53:54 2014 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Jun 05 09:09:53 2014 +0200
     2.3 @@ -95,6 +95,27 @@
     2.4  	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]
     2.5    ]
     2.6  *}
     2.7 +setup {*
     2.8 +KEStore_Elems.add_thes
     2.9 +  [make_thy @{theory}
    2.10 +    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.11 +  make_isa @{theory} ("IsacKnowledge", "Theorems")
    2.12 +    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.13 +  make_thm @{theory}  "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
    2.14 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.15 +  make_thm @{theory}  "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
    2.16 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.17 +  make_thm @{theory}  "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
    2.18 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.19 +  make_thm @{theory}  "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
    2.20 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.21 +  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
    2.22 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.23 +  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
    2.24 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
    2.25 +  make_thm @{theory}  "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
    2.26 +	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
    2.27 +*}
    2.28  
    2.29  (** problems **)
    2.30  setup {* KEStore_Elems.add_pbts

     3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Jun 05 08:53:54 2014 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Jun 05 09:09:53 2014 +0200
     3.3 @@ -125,6 +125,29 @@
     3.4    ]
     3.5  (*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
     3.6  *}
     3.7 +setup {*
     3.8 +KEStore_Elems.add_thes
     3.9 +  [make_thy @{theory "Diff"} ["Isabelle2011-->12"],
    3.10 +  make_isa @{theory "Diff"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
    3.11 +  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})
    3.12 +   ["Isabelle2011-->12"],
    3.13 +  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_cos_chain", prop_of @{thm diff_cos_chain})
    3.14 +   ["Isabelle2011-->12"],
    3.15 +  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
    3.16 +   ["Isabelle2011-->12"],
    3.17 +  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
    3.18 +   ["Isabelle2011-->12"],
    3.19 +  make_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
    3.20 +   ["Isabelle2011-->12"],
    3.21 +
    3.22 +  make_isa @{theory "Diff"} ("IsacKnowledge", "Rulesets") ["Isabelle2011-->12"],
    3.23 +  make_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"],
    3.24 +
    3.25 +  make_thy @{theory "Test"} ["Isabelle2011-->12"],
    3.26 +  make_isa @{theory "Test"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
    3.27 +  make_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute})
    3.28 +   ["Isabelle2011-->12"]]
    3.29 +*}
    3.30  
    3.31  subsection {* Add error patterns *}
    3.32  subsubsection {* Error patterns for differentiation *}
    3.33 @@ -156,6 +179,21 @@
    3.34       parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list)
    3.35    ]
    3.36  *}
    3.37 +setup {*
    3.38 +KEStore_Elems.add_thes
    3.39 +  [insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
    3.40 +    ([("fill-d_d-arg",
    3.41 +      parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    3.42 +    ("fill-both-args",
    3.43 +      parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    3.44 +    ("fill-d_d",
    3.45 +      parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
    3.46 +    ("fill-inner-deriv",
    3.47 +      parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
    3.48 +    ("fill-all",
    3.49 +      parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list)
    3.50 +  ]
    3.51 +*}
    3.52  
    3.53  subsubsection {* Error patterns for calculation with rationals *}
    3.54