isabelle: src/HOL/Isar_examples/ROOT.ML@1e4451999200 (annotated)

6444 2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	1	(* Title: HOL/Isar_examples/ROOT.ML
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	2	ID: $Id$
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	4
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	5	Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	6	*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm parents: diff changeset	7
7384 33c976216121 added MutilatedCheckerboard; wenzelm parents: 6882 diff changeset	8	time_use_thy "BasicLogic";
7800 8ee919e42174 improved presentation; wenzelm parents: 7621 diff changeset	9	time_use_thy "Cantor";
7384 33c976216121 added MutilatedCheckerboard; wenzelm parents: 6882 diff changeset	10	time_use_thy "Peirce";
33c976216121 added MutilatedCheckerboard; wenzelm parents: 6882 diff changeset	11	time_use_thy "ExprCompiler";
33c976216121 added MutilatedCheckerboard; wenzelm parents: 6882 diff changeset	12	time_use_thy "Group";
7443 e5356e73f57a renamed NatSum to Summation; wenzelm parents: 7436 diff changeset	13	time_use_thy "Summation";
7384 33c976216121 added MutilatedCheckerboard; wenzelm parents: 6882 diff changeset	14	time_use_thy "KnasterTarski";
8814 0a5edcbe0695 adapted to new arithmetic simprocs; wenzelm parents: 8782 diff changeset	15	time_use_thy "MutilatedCheckerboard";
12105 1e4451999200 tuned; wenzelm parents: 10257 diff changeset	16	with_path "../W0" (no_document time_use_thy) "Type";
1e4451999200 tuned; wenzelm parents: 10257 diff changeset	17	with_path "../W0" time_use_thy "W_correct";
1e4451999200 tuned; wenzelm parents: 10257 diff changeset	18	with_path "../NumberTheory" (no_document time_use_thy) "Primes";
9942 87f0809a06a9 moved Primes, Fib, Factorization to HOL/NumberTheory paulson parents: 8814 diff changeset	19	with_path "../NumberTheory" time_use_thy "Fibonacci";
8020 2823ce1753a5 added Isar_examples/Puzzle.thy; wenzelm parents: 7800 diff changeset	20	time_use_thy "Puzzle";
8675 a2ff2301d65e added NestedDatatype; wenzelm parents: 8137 diff changeset	21	time_use_thy "NestedDatatype";
10145 e44b8b7cb01b added Hoare; wenzelm parents: 9942 diff changeset	22	time_use_thy "HoareEx";

author	wenzelm
	Thu, 08 Nov 2001 23:50:08 +0100
changeset 12105	1e4451999200
parent 10257	21055ac27708
child 12946	75447c743810
permissions	-rw-r--r--