isabelle: src/HOL/SPARK/Examples/ROOT.ML@355d5438f5fb (annotated)

41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	1	use_thys
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	2	["Gcd/Greatest_Common_Divisor",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	3
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	4	"Liseq/Longest_Increasing_Subsequence",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	5
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	6	"RIPEMD-160/F",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	7	"RIPEMD-160/Hash",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	8	"RIPEMD-160/K_L",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	9	"RIPEMD-160/K_R",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	10	"RIPEMD-160/R_L",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	11	"RIPEMD-160/Round",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	12	"RIPEMD-160/R_R",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	13	"RIPEMD-160/S_L",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	14	"RIPEMD-160/S_R",
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	15
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	16	"Sqrt/Sqrt"];

author	huffman
	Wed, 17 Aug 2011 15:12:34 -0700
changeset 44262	355d5438f5fb
parent 41561	d1318f3c86ba
permissions	-rw-r--r--