| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Fri, 16 Jun 2000 13:13:55 +0200 |
paulson |
tracing flag for arith_tac
|
file |
diff |
annotate
|
| Wed, 07 Jun 2000 12:06:36 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:06:22 +0200 |
paulson |
added type constraint ::nat because 0 is now overloaded
|
file |
diff |
annotate
|
| Fri, 12 May 2000 14:59:12 +0200 |
paulson |
deleted some redundant simprules
|
file |
diff |
annotate
|
| Mon, 08 May 2000 16:58:18 +0200 |
paulson |
moved le_square, proved le_cube
|
file |
diff |
annotate
|
| Tue, 18 Apr 2000 15:56:41 +0200 |
paulson |
replaced obsolete diff_right_cancel by diff_diff_eq
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 15:18:02 +0200 |
paulson |
added some new iff-lemmas; removed some obsolete thms
|
file |
diff |
annotate
|
| Fri, 24 Mar 2000 20:59:15 +0100 |
wenzelm |
arith method: HEADGOAL;
|
file |
diff |
annotate
|
| Fri, 17 Mar 2000 17:11:59 +0100 |
wenzelm |
arith method: bang arg;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 16:23:34 +0100 |
wenzelm |
case_tac now subsumes both boolean and datatype cases;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 12:51:10 +0100 |
nipkow |
exhaust_tac -> cases_tac
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 16:13:19 +0100 |
paulson |
new lemmas
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 15:28:32 +0100 |
paulson |
new theorem nat_diff_split'
|
file |
diff |
annotate
|
| Wed, 05 Jan 2000 11:56:04 +0100 |
wenzelm |
replaced HOLogic.termTVar by HOLogic.termT;
|
file |
diff |
annotate
|