| Wed, 08 Aug 2012 11:21:09 +0200 |
hoelzl |
add legacy target for HOL-Probability, needed by AFP/Markov_Models
|
file |
diff |
annotate
|
| Wed, 08 Aug 2012 00:22:06 +0200 |
wenzelm |
more legacy targets;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 23:43:05 +0200 |
wenzelm |
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 14:43:55 +0200 |
kuncar |
Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 15:55:19 +0200 |
bulwahn |
moved another larger quickcheck example to Quickcheck_Benchmark
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 17:59:18 +0200 |
huffman |
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 15:42:39 +0200 |
huffman |
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 21:48:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 12:36:59 +0200 |
bulwahn |
moving a first Quickcheck example with many computations into a separate session Quickcheck_Benchmark
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 08:12:15 +0200 |
bulwahn |
moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 21:46:48 +0200 |
wenzelm |
reactivated HOL-NSA-Examples;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2012 09:56:34 +0200 |
haftmann |
library theories for debugging and parallel computing using code generation towards Isabelle/ML
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML files
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 19:38:39 +0200 |
haftmann |
removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renaming
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 13:59:39 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 13:54:37 +0200 |
bulwahn |
adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
moved MaSh into own files
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 18:41:34 +0200 |
bulwahn |
adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
|
file |
diff |
annotate
|
| Mon, 09 Jul 2012 10:04:07 +0200 |
bulwahn |
adding the hotel key card example in Quickcheck-Examples
|
file |
diff |
annotate
|
| Thu, 05 Jul 2012 13:24:09 +0200 |
haftmann |
Stub theory for division on functionals.
|
file |
diff |
annotate
|
| Mon, 02 Jul 2012 12:23:30 +0200 |
bulwahn |
adding some minimal documentation and an example of quickcheck's interfaces
|
file |
diff |
annotate
|
| Thu, 28 Jun 2012 09:14:57 +0200 |
Andreas Lochbihler |
add generic phantom type
|
file |
diff |
annotate
|
| Wed, 20 Jun 2012 16:54:08 +0200 |
Rafal Kolanski |
Integrated set comprehension pointfree simproc.
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 08:32:26 +0200 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
| Thu, 31 May 2012 16:58:38 +0200 |
Andreas Lochbihler |
unify Card_Univ and Cardinality
|
file |
diff |
annotate
|
| Mon, 28 May 2012 02:18:46 +0200 |
bulwahn |
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
|
file |
diff |
annotate
|
| Wed, 30 May 2012 16:05:06 +0200 |
Andreas Lochbihler |
remove pretty syntax for FinFuns at the end and provide separate syntax theory
|
file |
diff |
annotate
|
| Tue, 29 May 2012 15:31:58 +0200 |
Andreas Lochbihler |
move FinFuns from AFP to repository
|
file |
diff |
annotate
|
| Fri, 18 May 2012 16:43:38 +0200 |
blanchet |
added a timeout to "try0" in Mirabelle
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 15:24:37 +0200 |
blanchet |
get rid of old CASC setup and move the arithmetic part to a new theory
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 15:24:37 +0200 |
blanchet |
move file to where it belongs
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 13:59:29 +0100 |
sultana |
reversed Tools to Actions Mirabelle renaming;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 11:05:04 +0200 |
huffman |
new example theory for quotient/transfer
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 13:49:31 +0200 |
huffman |
new example theory for transfer package
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 20:19:13 +0200 |
nipkow |
added revised version of Abs_Int
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 17:32:30 +0200 |
nipkow |
reorganised IMP
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 16:21:47 +1000 |
Thomas Sewell |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 23:52:17 +0100 |
sultana |
renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 19:29:31 +0200 |
krauss |
removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 22:31:00 +0200 |
huffman |
new transfer proof method
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 22:04:50 +0200 |
huffman |
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 20:56:32 +0200 |
huffman |
merged
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 15:15:00 +0200 |
huffman |
modernized obsolete old-style theory name with proper new-style underscore
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:48:16 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:53:32 +0200 |
wenzelm |
some context examples;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 23:21:54 +0200 |
krauss |
merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 22:41:56 +0200 |
krauss |
renamed import session back to Import, conforming to directory name; NEWS
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 23:07:15 +0200 |
wenzelm |
more precise IsaMakefile (eg. see HOL-Algebra);
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 22:14:59 +0200 |
krauss |
merged
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 22:03:45 +0200 |
krauss |
removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 14:50:47 +0200 |
Cezary Kaliszyk |
Modernized HOL-Import for HOL Light
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 16:09:58 +0200 |
huffman |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 18:56:02 +0200 |
haftmann |
dropped now obsolete Cset theories
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 14:27:29 +0200 |
huffman |
remove content-free theory ex/Arithmetic_Series_Complex.thy
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:44:01 +0200 |
bulwahn |
adding theory to prove completeness of the exhaustive generators
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 20:09:18 +0200 |
huffman |
revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 19:18:03 +0200 |
wenzelm |
disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 12:52:40 +0100 |
wenzelm |
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:20:07 +0100 |
wenzelm |
more precise TPTP keywords and dependencies;
|
file |
diff |
annotate
|
| Wed, 07 Mar 2012 14:30:35 +0100 |
wenzelm |
some recovery of IsaMakefile targets from f3c10e908f65;
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 10:34:44 +0100 |
haftmann |
move test targets to test target
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 10:33:47 +0100 |
haftmann |
dropped images for importer sessions
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 00:27:07 +0100 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 23:42:56 +0100 |
haftmann |
added actual dependencies
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 22:38:33 +0100 |
haftmann |
switch of target Import-HOL_Light-Imported: not operative at the moment
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:42:41 +0100 |
haftmann |
formal infrastructure for import sessions
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 23:30:38 +0100 |
wenzelm |
removed dead code (cf. a34d89ce6097);
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 12:12:28 +0100 |
wenzelm |
reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 22:46:44 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 19:45:10 +0100 |
wenzelm |
more precise clean target;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 11:23:34 +0100 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 09:40:02 +0100 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 21:25:59 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Wed, 22 Feb 2012 18:08:27 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 22 Feb 2012 17:25:35 +0100 |
bulwahn |
adding some examples with find_unused_assms command
|
file |
diff |
annotate
|
| Wed, 22 Feb 2012 08:01:41 +0100 |
bulwahn |
moving Quickcheck's example to its own session
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 09:17:53 +0100 |
huffman |
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 10:12:11 +0100 |
bulwahn |
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
added problem importer
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed theory exporter
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:31 +0100 |
blanchet |
rebranded Nitrox, for more uniformity
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 10:45:42 +0100 |
bulwahn |
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 09:38:30 +0100 |
bulwahn |
renamed theory AList to DAList
|
file |
diff |
annotate
|
| Mon, 16 Jan 2012 07:46:58 +0100 |
nipkow |
missing dependency
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 10:17:07 +0100 |
bulwahn |
adding theory association lists with invariant
|
file |
diff |
annotate
|
| Sat, 07 Jan 2012 20:18:56 +0100 |
haftmann |
dropped theory More_Set
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 20:39:50 +0100 |
haftmann |
farewell to theory More_List
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
incorporated More_Set and More_List into the Main body -- to be consolidated later
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 17:40:43 +0100 |
haftmann |
dropped Executable_Set wrapper theory
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 12:42:10 +0100 |
wenzelm |
clarified modules that contribute to datatype package;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 10:52:35 +0100 |
wenzelm |
clarified modules that contribute to datatype package;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 17:37:14 +0100 |
wenzelm |
separate rep_datatype.ML;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 09:13:32 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 09:13:23 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 18:07:32 +0100 |
blanchet |
added new proof redirection code
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 16:30:32 +0100 |
bulwahn |
correcting dependencies after renaming
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 12:02:02 +0100 |
wenzelm |
more visible benchmarks;
|
file |
diff |
annotate
|
| Sun, 11 Dec 2011 18:22:06 +0100 |
nipkow |
added IMP/Live_True.thy
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 14:46:18 +0100 |
kuncar |
added dependencies
|
file |
diff |
annotate
|
| Sun, 04 Dec 2011 18:30:57 +0100 |
huffman |
merged
|
file |
diff |
annotate
|
| Sun, 04 Dec 2011 13:10:19 +0100 |
huffman |
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
|
file |
diff |
annotate
|
| Sun, 04 Dec 2011 18:29:29 +0100 |
nipkow |
missing dependency
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 20:52:16 +0100 |
nipkow |
merged IMP/Util into IMP/Vars
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 22:45:21 +0100 |
wenzelm |
more conventional file name;
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 13:50:01 +0100 |
bulwahn |
adding another example for lifting definitions
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 19:01:05 +0100 |
bulwahn |
adding a preliminary example to show how the quotient_definition package can be generalized
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 11:50:52 +0100 |
hoelzl |
add Code_Real_Approx_By_Float
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 16:22:26 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 10:29:05 +1100 |
kleing |
moved latex generation for HOL-IMP out of distribution
|
file |
diff |
annotate
|
| Tue, 01 Nov 2011 10:05:28 +0100 |
bulwahn |
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
|
file |
diff |
annotate
|
| Tue, 25 Oct 2011 16:37:11 +0200 |
bulwahn |
renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library
|
file |
diff |
annotate
|
| Mon, 24 Oct 2011 10:45:54 +0200 |
nipkow |
latex output not needed because errors manifest themselves earlier
|
file |
diff |
annotate
|
| Sat, 22 Oct 2011 20:17:50 +0200 |
nipkow |
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
|
file |
diff |
annotate
|