222 (qualify (Binding.make ("Abst", \<^here>)), typ "('a \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), |
222 (qualify (Binding.make ("Abst", \<^here>)), typ "('a \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), |
223 (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), |
223 (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), |
224 (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
224 (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
225 (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
225 (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
226 (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn), |
226 (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn), |
227 (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", Mixfix.mixfix "?")] |
227 (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)] |
228 #> add_deps_const "Pure.eq" |
228 #> add_deps_const "Pure.eq" |
229 #> add_deps_const "Pure.imp" |
229 #> add_deps_const "Pure.imp" |
230 #> add_deps_const "Pure.all" |
230 #> add_deps_const "Pure.all" |
231 #> add_deps_const "Pure.type" |
231 #> add_deps_const "Pure.type" |
232 #> add_deps_const "Pure.dummy_pattern" |
232 #> add_deps_const "Pure.dummy_pattern" |