| Sun, 22 Apr 2012 11:05:04 +0200 |
new example theory for quotient/transfer
|
file | diff | annotate |
| Sat, 21 Apr 2012 13:49:31 +0200 |
new example theory for transfer package
|
file | diff | annotate |
| Thu, 19 Apr 2012 20:19:13 +0200 |
added revised version of Abs_Int
|
file | diff | annotate |
| Thu, 19 Apr 2012 17:32:30 +0200 |
reorganised IMP
|
file | diff | annotate |
| Tue, 17 Apr 2012 16:21:47 +1000 |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file | diff | annotate |
| Sat, 14 Apr 2012 23:52:17 +0100 |
renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
|
file | diff | annotate |
| Sat, 14 Apr 2012 19:29:31 +0200 |
removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
|
file | diff | annotate |
| Tue, 03 Apr 2012 22:31:00 +0200 |
new transfer proof method
|
file | diff | annotate |
| Tue, 03 Apr 2012 22:04:50 +0200 |
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
|
file | diff | annotate |
| Tue, 03 Apr 2012 20:56:32 +0200 |
merged
|
file | diff | annotate |
| Tue, 03 Apr 2012 15:15:00 +0200 |
modernized obsolete old-style theory name with proper new-style underscore
|
file | diff | annotate |
| Tue, 03 Apr 2012 17:48:16 +0200 |
merged
|
file | diff | annotate |
| Tue, 03 Apr 2012 16:53:32 +0200 |
some context examples;
|
file | diff | annotate |
| Tue, 03 Apr 2012 16:26:48 +0200 |
new package Lifting - initial commit
|
file | diff | annotate |
| Sun, 01 Apr 2012 23:21:54 +0200 |
merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
|
file | diff | annotate |
| Sun, 01 Apr 2012 22:41:56 +0200 |
renamed import session back to Import, conforming to directory name; NEWS
|
file | diff | annotate |
| Sun, 01 Apr 2012 23:07:15 +0200 |
more precise IsaMakefile (eg. see HOL-Algebra);
|
file | diff | annotate |
| Sun, 01 Apr 2012 22:14:59 +0200 |
merged
|
file | diff | annotate |
| Sun, 01 Apr 2012 22:03:45 +0200 |
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 |
Modernized HOL-Import for HOL Light
|
file | diff | annotate |
| Sun, 01 Apr 2012 16:09:58 +0200 |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file | diff | annotate |
| Fri, 30 Mar 2012 18:56:02 +0200 |
dropped now obsolete Cset theories
|
file | diff | annotate |
| Fri, 30 Mar 2012 14:27:29 +0200 |
remove content-free theory ex/Arithmetic_Series_Complex.thy
|
file | diff | annotate |
| Fri, 30 Mar 2012 08:44:01 +0200 |
adding theory to prove completeness of the exhaustive generators
|
file | diff | annotate |
| Mon, 26 Mar 2012 20:09:18 +0200 |
revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
|
file | diff | annotate |
| Mon, 26 Mar 2012 19:18:03 +0200 |
disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;
|
file | diff | annotate |
| Sun, 25 Mar 2012 20:15:39 +0200 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| Sat, 17 Mar 2012 12:52:40 +0100 |
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
|
file | diff | annotate |
| Thu, 15 Mar 2012 22:20:07 +0100 |
more precise TPTP keywords and dependencies;
|
file | diff | annotate |
| Wed, 07 Mar 2012 14:30:35 +0100 |
some recovery of IsaMakefile targets from f3c10e908f65;
|
file | diff | annotate |
| Sun, 04 Mar 2012 10:34:44 +0100 |
move test targets to test target
|
file | diff | annotate |
| Sun, 04 Mar 2012 10:33:47 +0100 |
dropped images for importer sessions
|
file | diff | annotate |
| Sun, 04 Mar 2012 00:27:07 +0100 |
more accurate dependencies
|
file | diff | annotate |
| Sat, 03 Mar 2012 23:42:56 +0100 |
added actual dependencies
|
file | diff | annotate |
| Sat, 03 Mar 2012 22:38:33 +0100 |
switch of target Import-HOL_Light-Imported: not operative at the moment
|
file | diff | annotate |
| Sat, 03 Mar 2012 21:42:41 +0100 |
formal infrastructure for import sessions
|
file | diff | annotate |
| Mon, 27 Feb 2012 23:30:38 +0100 |
removed dead code (cf. a34d89ce6097);
|
file | diff | annotate |
| Mon, 27 Feb 2012 12:12:28 +0100 |
reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
|
file | diff | annotate |
| Fri, 24 Feb 2012 22:46:44 +0100 |
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 |
more precise clean target;
|
file | diff | annotate |
| Fri, 24 Feb 2012 11:23:34 +0100 |
renamed 'try_methods' to 'try0'
|
file | diff | annotate |
| Fri, 24 Feb 2012 09:40:02 +0100 |
given up disfruitful branch
|
file | diff | annotate |
| Thu, 23 Feb 2012 21:25:59 +0100 |
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 |
NEWS
|
file | diff | annotate |
| Wed, 22 Feb 2012 17:25:35 +0100 |
adding some examples with find_unused_assms command
|
file | diff | annotate |
| Wed, 22 Feb 2012 08:01:41 +0100 |
moving Quickcheck's example to its own session
|
file | diff | annotate |
| Tue, 21 Feb 2012 09:17:53 +0100 |
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
|
file | diff | annotate |
| Thu, 02 Feb 2012 10:12:11 +0100 |
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 |
added problem importer
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed theory exporter
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed two files to make room for a new file
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:31 +0100 |
rebranded Nitrox, for more uniformity
|
file | diff | annotate |
| Tue, 17 Jan 2012 10:45:42 +0100 |
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 |
renamed theory AList to DAList
|
file | diff | annotate |
| Mon, 16 Jan 2012 07:46:58 +0100 |
missing dependency
|
file | diff | annotate |
| Tue, 10 Jan 2012 10:17:07 +0100 |
adding theory association lists with invariant
|
file | diff | annotate |
| Sat, 07 Jan 2012 20:18:56 +0100 |
dropped theory More_Set
|
file | diff | annotate |
| Fri, 06 Jan 2012 20:39:50 +0100 |
farewell to theory More_List
|
file | diff | annotate |
| Mon, 26 Dec 2011 22:17:10 +0100 |
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 |
dropped Executable_Set wrapper theory
|
file | diff | annotate |