Tue, 27 Oct 2009 14:59:00 +0100 |
Cezary Kaliszyk |
Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 11:27:53 +0100 |
Christian Urban |
made quotients compatiple with Nominal; updated keyword file
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 11:03:38 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 09:01:12 +0100 |
Cezary Kaliszyk |
Completely cleaned Int.
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 07:46:52 +0100 |
Cezary Kaliszyk |
Further reordering in Int code.
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 19:35:30 +0100 |
Cezary Kaliszyk |
Simplifying Int.
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 15:32:17 +0100 |
Cezary Kaliszyk |
Merge
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 15:31:53 +0100 |
Cezary Kaliszyk |
Simplifying Int and Working on map
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 14:18:26 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 14:16:32 +0100 |
Cezary Kaliszyk |
Simplifying code in int
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 13:33:28 +0100 |
Cezary Kaliszyk |
Symmetry of integer addition
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 01:31:04 +0200 |
Christian Urban |
added "print_quotients" command to th ekeyword file
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 22:52:23 +0200 |
Christian Urban |
added another example file about integers (see HOL/Int.thy)
|
file |
diff |
annotate
|