| Sat, 12 Oct 2019 16:46:33 +0200 |
wenzelm |
early setup of proof preprocessing;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 22:01:45 +0200 |
wenzelm |
proper ML names;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2019 20:09:25 +0200 |
wenzelm |
clarified global theory context;
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 13:28:32 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 15:38:25 +0200 |
nipkow |
swap False to the right in assumptions to be eliminated at the right end
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 19:09:28 +0200 |
nipkow |
undid 6d7b7a037e8d
|
file |
diff |
annotate
|
| Sat, 25 Apr 2015 17:38:22 +0200 |
nipkow |
new ==> simp rule
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 16:47:55 +0200 |
nipkow |
prepared for more meta-simp rules (by Stefan Berghofer)
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 23:14:05 +0200 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
added 'extraction' plugins -- this might help 'HOL-Proofs'
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 16:11:01 +0200 |
blanchet |
'code' is needed for extraction datatype
|
file |
diff |
annotate
|