isabelle: src/HOL/Decision_Procs/Decision_Procs.thy@2c46f628e6b7 (annotated)

33356 9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33152 diff changeset	1	header {* Various decision procedures, typically involving reflection *}
30429 39acdf031548 moved Decision_Procs examples to Decision_Procs/ex haftmann parents: 29825 diff changeset	2
29825 384e47590e7f added Decision_Procs.thy haftmann parents: diff changeset	3	theory Decision_Procs
33356 9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33152 diff changeset	4	imports
35044 7c761a4bd91f tuned header haftmann parents: 33356 diff changeset	5	Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order
7c761a4bd91f tuned header haftmann parents: 33356 diff changeset	6	Parametric_Ferrante_Rackoff
33356 9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33152 diff changeset	7	Commutative_Ring_Complete
9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33152 diff changeset	8	"ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex"
29825 384e47590e7f added Decision_Procs.thy haftmann parents: diff changeset	9	begin
384e47590e7f added Decision_Procs.thy haftmann parents: diff changeset	10
36347 0ca616bc6c6f line break haftmann parents: 35044 diff changeset	11	end