src/Pure/pure_thy.ML
changeset 70403 468cfd56ee03
parent 70388 e31271559de8
child 71155 25b872d1d421
equal deleted inserted replaced
70402:29d81b53c40b 70403:468cfd56ee03
   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"