2010-02-12 |
Cezary Kaliszyk |
renamed 'as' to 'is' everywhere.
|
file |
diff |
annotate
|
2010-02-12 |
Cezary Kaliszyk |
The lattice instantiations are gone from Isabelle/Main, so
|
file |
diff |
annotate
|
2010-02-11 |
Cezary Kaliszyk |
Main renaming + fixes for new Isabelle in IntEx2.
|
file |
diff |
annotate
|
2010-01-21 |
Cezary Kaliszyk |
Changed fun_map and rel_map to definitions.
|
file |
diff |
annotate
|
2009-12-26 |
Christian Urban |
generalised absrep function; needs consolidation
|
file |
diff |
annotate
|
2009-12-19 |
Christian Urban |
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
|
file |
diff |
annotate
|
2009-12-19 |
Christian Urban |
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
|
file |
diff |
annotate
|
2009-12-11 |
Cezary Kaliszyk |
Renaming
|
file |
diff |
annotate
|
2009-12-11 |
Christian Urban |
added Int example from Larry
|
file |
diff |
annotate
|
2009-12-11 |
Cezary Kaliszyk |
More theorem renaming.
|
file |
diff |
annotate
|
2009-12-11 |
Cezary Kaliszyk |
Renamed theorems in IntEx2 to conform to names in Int.
|
file |
diff |
annotate
|
2009-12-11 |
Cezary Kaliszyk |
New syntax for definitions.
|
file |
diff |
annotate
|
2009-12-10 |
Cezary Kaliszyk |
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
|
file |
diff |
annotate
|
2009-12-10 |
Cezary Kaliszyk |
Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
|
file |
diff |
annotate
|
2009-12-10 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-10 |
Cezary Kaliszyk |
With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
|
file |
diff |
annotate
|
2009-12-10 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-10 |
Christian Urban |
naming in this file cannot be made to agree to the original (PROBLEM?)
|
file |
diff |
annotate
|
2009-12-10 |
Cezary Kaliszyk |
Lifted some kind of induction.
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
more proofs in IntEx2
|
file |
diff |
annotate
|
2009-12-09 |
Cezary Kaliszyk |
Finished one proof in IntEx2.
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
slightly more on IntEx2
|
file |
diff |
annotate
|
2009-12-09 |
Christian Urban |
proved (with a lot of pain) that times_raw is respectful
|
file |
diff |
annotate
|
2009-12-09 |
Cezary Kaliszyk |
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
tuned the examples and flagged the problematic cleaning lemmas in FSet
|
file |
diff |
annotate
|
2009-12-08 |
Christian Urban |
changed names of attributes
|
file |
diff |
annotate
|
2009-12-07 |
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
|
2009-12-07 |
Christian Urban |
isabelle make tests all examples
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
added "end" to each example theory
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
List moved after QuotMain
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
directory re-arrangement
|
file |
diff |
annotate
| base
|