isabelle: src/HOL/SPARK/Examples/ROOT.ML@df7554ebe024 (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	kleing
	Thu, 03 Nov 2011 18:10:13 +1100
changeset 45323	df7554ebe024
parent 41561	d1318f3c86ba
permissions	-rw-r--r--