| Thu, 29 Apr 2010 09:06:35 +0200 |
Cezary Kaliszyk |
Tuning the quotient examples
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:25:32 +0200 |
blanchet |
merge
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 18:11:41 +0200 |
blanchet |
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 17:38:25 +0200 |
blanchet |
move the minimizer to the Sledgehammer directory
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 13:31:52 -0700 |
huffman |
document generation for Multivariate_Analysis
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 11:11:09 -0700 |
huffman |
move l2-norm stuff into separate theory file
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:36:04 +0200 |
wenzelm |
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 10:00:53 +0200 |
Cezary Kaliszyk |
Finite set theory
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 22:01:06 +0200 |
wenzelm |
split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 12:27:14 +0200 |
haftmann |
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 17:46:42 +0200 |
haftmann |
removed rather toyish tree
|
file |
diff |
annotate
|
| Thu, 08 Apr 2010 08:17:27 +0200 |
bulwahn |
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 17:24:44 +0200 |
hoelzl |
Added Information theory and Example: dining cryptographers
|
file |
diff |
annotate
|
| Thu, 01 Apr 2010 15:37:30 +0200 |
wenzelm |
slightly more standard dependencies;
|
file |
diff |
annotate
|
| Thu, 01 Apr 2010 10:27:06 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 15:50:18 +0200 |
blanchet |
get rid of Polyhash, since it's no longer used
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 14:49:53 +0200 |
blanchet |
reintroduce efficient set structure to collect "no_atp" theorems
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
putting compilation setup of predicate compiler in a separate file
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:52 +0200 |
bulwahn |
adding specialisation of predicates to the predicate compiler
|
file |
diff |
annotate
|
| Thu, 25 Mar 2010 17:56:31 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:31:37 +0100 |
blanchet |
add new file "sledgehammer_util.ML" to setup
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 22:30:33 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:41:25 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:44 +0100 |
bulwahn |
removed predicate_compile_core.ML from HOL-ex session
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:44 +0100 |
bulwahn |
added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:43 +0100 |
bulwahn |
moved further predicate compile files to HOL-Library
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:43 +0100 |
bulwahn |
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:30:21 +0100 |
boehmes |
more precise dependencies
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 09:44:47 +0100 |
boehmes |
cache_io is now just a single ML file instead of a component
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 19:35:03 +0100 |
wenzelm |
more accurate dependencies;
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 16:17:41 +0100 |
hoelzl |
Generate image for HOL-Probability
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 13:48:15 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
removed unused Predicate_Compile_Set
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 15:07:44 +0100 |
blanchet |
move the Sledgehammer Isar commands together into one file;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
| Tue, 16 Mar 2010 16:27:28 +0100 |
hoelzl |
Added product measure space
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:37:44 +0100 |
blanchet |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 18:16:31 +0100 |
blanchet |
move Sledgehammer files in a directory of their own
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 17:19:12 +0100 |
wenzelm |
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 17:39:45 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 14:39:58 +0100 |
haftmann |
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 16:53:27 +0100 |
haftmann |
split off theory Big_Operators from theory Finite_Set
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 16:00:51 -0800 |
huffman |
remove obsolete theory Nat_Int_Bij
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 14:57:13 -0800 |
huffman |
new theory Library/Nat_Bijection.thy
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 15:31:30 +0100 |
haftmann |
added Table.thy
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 21:52:26 +0100 |
hoelzl |
Add Lebesgue integral and probability space.
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 22:13:32 +0100 |
bulwahn |
adding HOL-Mutabelle to tests
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:45:10 +0100 |
krauss |
removed obsolete helper theory
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:34:40 +0100 |
haftmann |
renamed theory Rational to Rat
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 17:55:00 +0100 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 17:33:03 +0100 |
hoelzl |
Moved old Integration to examples.
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 14:11:32 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 10:11:31 +0100 |
haftmann |
dropped session W0; c.f. MiniML in AFP
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 08:04:07 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 16:03:44 +0100 |
haftmann |
added missing separator
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
distributed theory Algebras to theories Groups and Lattices
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 20:41:49 +0100 |
hoelzl |
Replaced Integration by Multivariate-Analysis/Real_Integration
|
file |
diff |
annotate
|
| Sat, 20 Feb 2010 23:23:04 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 15:25:36 +0100 |
boehmes |
added Cache_IO: cache for output of external tools,
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 19:37:34 +0100 |
wenzelm |
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:02 +0100 |
haftmann |
revert uninspired Structure_Syntax experiment
|
file |
diff |
annotate
|
| Tue, 09 Feb 2010 17:06:05 +0100 |
blanchet |
merged (manual for "nitpick_hol.ML" and "kodkod.ML")
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:27:21 +0100 |
blanchet |
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
|
file |
diff |
annotate
|
| Thu, 04 Feb 2010 16:03:15 +0100 |
blanchet |
split "nitpick_hol.ML" into two files to make it more manageable;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 21:26:52 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:08:32 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:41 +0100 |
haftmann |
separate library theory for type classes combining lattices with various algebraic structures
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 10:36:02 +0100 |
haftmann |
separate theory for index structures
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 19:30:08 +0100 |
boehmes |
updated dependencies
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Mon, 25 Jan 2010 16:19:42 +0100 |
bulwahn |
adding Mutabelle to repository
|
file |
diff |
annotate
|
| Fri, 22 Jan 2010 15:26:29 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Wed, 20 Jan 2010 11:56:45 +0100 |
bulwahn |
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
|
file |
diff |
annotate
|
| Fri, 22 Jan 2010 13:38:29 +0100 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
file |
diff |
annotate
|
| Tue, 29 Dec 2009 16:20:39 +0100 |
wenzelm |
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
|
file |
diff |
annotate
|
| Fri, 18 Dec 2009 12:00:29 +0100 |
blanchet |
polished Nitpick's binary integer support etc.;
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 15:36:05 +0100 |
boehmes |
updated dependencies
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 15:06:12 +0100 |
boehmes |
depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 16:27:48 +0100 |
haftmann |
split off evaluation mechanisms in separte module Code_Eval
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 14:54:01 +0100 |
haftmann |
merged Crude_Executable_Set into Executable_Set
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 12:22:09 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 11:42:49 +0100 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 08:41:10 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 14:37:23 +0100 |
haftmann |
backported parts of abstract byte code verifier from AFP/Jinja
|
file |
diff |
annotate
|
| Wed, 02 Dec 2009 17:53:34 +0100 |
haftmann |
added Crude_Executable_Set.thy
|
file |
diff |
annotate
|
| Fri, 20 Nov 2009 15:33:10 +0100 |
wenzelm |
load ML directly into theory Code_Generator (quickcheck also requires this);
|
file |
diff |
annotate
|
| Wed, 18 Nov 2009 09:34:53 +0100 |
boehmes |
added arithmetic example using div and mod
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 18:52:30 +0100 |
hoelzl |
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
|
file |
diff |
annotate
|
| Sat, 14 Nov 2009 19:56:18 +0100 |
wenzelm |
moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 20:38:57 +0100 |
bulwahn |
added a tabled implementation of the reflexive transitive closure
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 13:54:00 +0100 |
blanchet |
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 11:58:36 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:08:51 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 15:26:00 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 12:09:32 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 18:09:30 +0100 |
blanchet |
merged my Auto Nitpick change with Lukas's Predicate Compiler changes
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 17:43:43 +0100 |
blanchet |
introduced Auto Nitpick in addition to Auto Quickcheck;
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 15:50:15 +0000 |
paulson |
New theory Probability/Borel.thy, and some associated lemmas
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 14:42:42 +0100 |
krauss |
renamed method induct_scheme to induction_schema
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 13:42:29 +0100 |
krauss |
removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 16:23:51 +0100 |
wenzelm |
more accurate cleanup;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 15:55:07 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 15:54:14 +0100 |
wenzelm |
more accurate dependencies;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 15:44:39 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 15:24:49 +0100 |
boehmes |
handle let expressions inside terms by unfolding (instead of raising an exception),
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:48:40 +0100 |
boehmes |
shorter names for variables and verification conditions,
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:37:39 +0100 |
wenzelm |
more accurate dependencies;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 17:17:30 +0100 |
krauss |
added Tree23 to IsaMakefile
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 17:54:24 +0100 |
boehmes |
added HOL-Boogie
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 13:59:49 +0100 |
haftmann |
moved Commutative_Ring into session Decision_Procs
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 01:32:06 +0100 |
krauss |
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 18:17:26 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:06:15 +0100 |
wenzelm |
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 08:14:39 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|