| Mon, 23 Dec 2013 14:24:22 +0100 |
haftmann |
dropped redundant lemma
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:21 +0100 |
haftmann |
syntactically tuned
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:20 +0100 |
haftmann |
prefer plain bool over dedicated type for binary digits
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 20:46:36 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
generalized of_bool conversion
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
separated bit operations on type bit from generic syntactic bit operations
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
more lemmas on division
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 23:37:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:29:50 +0200 |
haftmann |
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:21:06 +0100 |
kuncar |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
file |
diff |
annotate
|
| Tue, 26 Feb 2013 20:09:25 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|