Lines Matching defs:body
245 arity:arity, body:theory_body_elem list}
261 body: theory_body_elem list
591 Instantiation { names=ns,arity=a,body=b })
602 body = b})
709 (* create a theory from a string of its body *)
710 fun theory_of_string body parents =
713 val text = unlines ["theory "^name,"begin",body,"end"]
746 val body = Term.strip_qnt_body qnt tm
749 in Term.subst_bounds (List.rev vars, body) end
905 val body = List.map (fn (pats,tm) => Pretty.quote (Pretty.block
910 in Pretty.block (head@Pretty.separate " | " body) end