| Thu, 21 Jan 2010 19:52:46 +0100 |
Cezary Kaliszyk |
Changed fun_map and rel_map to definitions.
|
file |
diff |
annotate
|
| Sat, 26 Dec 2009 07:15:30 +0100 |
Christian Urban |
generalised absrep function; needs consolidation
|
file |
diff |
annotate
|
| Sun, 20 Dec 2009 00:53:35 +0100 |
Christian Urban |
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
|
file |
diff |
annotate
|
| Sun, 20 Dec 2009 00:26:53 +0100 |
Christian Urban |
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 17:19:38 +0100 |
Cezary Kaliszyk |
Renaming
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 15:58:15 +0100 |
Christian Urban |
added Int example from Larry
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 11:30:00 +0100 |
Cezary Kaliszyk |
More theorem renaming.
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 11:25:52 +0100 |
Cezary Kaliszyk |
Renamed theorems in IntEx2 to conform to names in Int.
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 11:08:58 +0100 |
Cezary Kaliszyk |
New syntax for definitions.
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 08:55:30 +0100 |
Cezary Kaliszyk |
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 08:44:01 +0100 |
Cezary Kaliszyk |
Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 03:25:42 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 02:42:09 +0100 |
Cezary Kaliszyk |
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 01:48:39 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 01:47:55 +0100 |
Christian Urban |
naming in this file cannot be made to agree to the original (PROBLEM?)
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 01:39:47 +0100 |
Cezary Kaliszyk |
Lifted some kind of induction.
|
file |
diff |
annotate
|
| Wed, 09 Dec 2009 23:32:16 +0100 |
Christian Urban |
more proofs in IntEx2
|
file |
diff |
annotate
|
| Wed, 09 Dec 2009 22:43:11 +0100 |
Cezary Kaliszyk |
Finished one proof in IntEx2.
|
file |
diff |
annotate
|
| Wed, 09 Dec 2009 22:05:11 +0100 |
Christian Urban |
slightly more on IntEx2
|
file |
diff |
annotate
|
| Wed, 09 Dec 2009 20:35:52 +0100 |
Christian Urban |
proved (with a lot of pain) that times_raw is respectful
|
file |
diff |
annotate
|
| Wed, 09 Dec 2009 15:57:47 +0100 |
Cezary Kaliszyk |
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
|
file |
diff |
annotate
|
| Wed, 09 Dec 2009 00:03:18 +0100 |
Christian Urban |
tuned the examples and flagged the problematic cleaning lemmas in FSet
|
file |
diff |
annotate
|
| Tue, 08 Dec 2009 17:30:00 +0100 |
Christian Urban |
changed names of attributes
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 21:53:50 +0100 |
Christian Urban |
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 15:21:51 +0100 |
Christian Urban |
isabelle make tests all examples
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 14:37:10 +0100 |
Christian Urban |
added "end" to each example theory
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 14:35:45 +0100 |
Cezary Kaliszyk |
List moved after QuotMain
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 14:09:50 +0100 |
Christian Urban |
directory re-arrangement
|
file |
diff |
annotate
| base
|