isabelle: src/HOL/SPARK/Examples/ROOT.ML@21c42b095c84 (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	wenzelm
	Sun, 20 May 2012 11:34:33 +0200
changeset 47884	21c42b095c84
parent 41561	d1318f3c86ba
permissions	-rw-r--r--