| 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
|
| 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
|