Structure ratUtils


Source File Identifier index Theory binding index

signature ratUtils =
sig
	type term = Term.term
	type thm = Thm.thm
	type goal = Abbrev.goal
	type conv = Abbrev.conv
	type tactic = Abbrev.tactic

	val dest_rat : term -> term * term list
	val extract_rat : term -> term list

	val extract_rat_vars : term -> term list
	val extract_rat_equations : term -> term list
	val extract_rat_minv : term -> term list

end;

Source File Identifier index Theory binding index

HOL 4, Kananaskis-10