isabelle: src/HOL/SPARK/Examples/ROOT.ML@5438d88b2cb7 (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	blanchet
	Fri, 26 Aug 2011 10:12:17 +0200
changeset 44508	5438d88b2cb7
parent 41561	d1318f3c86ba
permissions	-rw-r--r--