Lines Matching defs:add_def
69 fun add_def tm =
75 fun define_const {Thy="bool",Name="~"} tm = add_def(``$~ = ^tm``)
76 | define_const {Thy="bool",Name="!"} tm = add_def(``$! = ^tm``)
77 | define_const {Thy="bool",Name="?"} tm = add_def(``$? = ^tm``)
78 | define_const {Thy="bool",Name="?!"} tm = add_def(``$?! = ^tm``)
79 | define_const {Thy="bool",Name="\\/"} tm = add_def(``$\/ = ^tm``)
80 | define_const {Thy="bool",Name="/\\"} tm = add_def(``$/\ = ^tm``)
81 | define_const {Thy="bool",Name="T"} tm = add_def(``T = ^tm``)
82 | define_const {Thy="bool",Name="F"} tm = add_def(``F = ^tm``)
83 | define_const {Thy="bool",Name="COND"} tm = add_def(``COND = ^tm``)
84 | define_const {Thy="min",Name="==>"} tm = add_def(``$==> = ^tm``)
123 val LET_DEF = add_def(concl LET_DEF)
124 val IN_DEF = add_def(concl IN_DEF)
125 val literal_case_DEF = add_def(concl literal_case_DEF)
126 val TYPE_DEFINITION = add_def(concl TYPE_DEFINITION)
127 val ARB_DEF = add_def(concl (REFL``ARB``))