| 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
|
| Fri, 21 Oct 2011 08:42:11 +0200 |
huffman |
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:20 +0200 |
bulwahn |
removing old code generator
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:25 +0200 |
bulwahn |
removing old code generator for inductive predicates
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:16 +0200 |
bulwahn |
removing old code generator setup in the HOL theory
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:15 +0200 |
bulwahn |
removing invocations of the evaluation method based on the old code generator
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 09:59:55 +0200 |
nipkow |
Added dependecies
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 09:55:11 +0200 |
nipkow |
Added Hoare-like Abstract Interpretation
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 08:51:55 +0200 |
nipkow |
moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 20:39:18 +0200 |
wenzelm |
reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
|
file |
diff |
annotate
|
| Sun, 25 Sep 2011 09:37:33 +0200 |
haftmann |
Quotient_Set.thy is part of library
|
file |
diff |
annotate
|
| Sat, 24 Sep 2011 00:17:32 +0100 |
sultana |
fixed IsaMakefile action for HOL-TPTP.
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 18:23:38 +0200 |
berghofe |
Moved extraction part of Higman's lemma to separate theory to allow reuse in
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 16:50:23 +0200 |
berghofe |
Added documentation for HOL-SPARK
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 15:55:16 +0200 |
blanchet |
reintroduced Minipick as Nitpick example
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 07:03:16 +0200 |
nipkow |
added missing makefile dependence
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 05:47:11 +0200 |
nipkow |
New proof method "induction" that gives induction hypotheses the name IH.
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 13:39:33 +0200 |
wenzelm |
finite sequences as useful as introductory example;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 09:28:03 +0200 |
bulwahn |
correcting theory name and dependencies
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 10:57:58 +0200 |
bulwahn |
moving connection of association lists to Mappings into a separate theory
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 23:38:52 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 19:25:44 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 19:25:18 +0200 |
nipkow |
Added Abstract Interpretation theories
|
file |
diff |
annotate
|