| Thu, 17 Jan 2019 15:50:28 +0000 |
Angeliki KoutsoukouArgyraki |
more tagging
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 21:27:33 +0000 |
Angeliki KoutsoukouArgyraki |
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 11:48:06 +0100 |
nipkow |
Reorg of material
|
file |
diff |
annotate
|
| Tue, 15 Jan 2019 21:31:20 +0100 |
nipkow |
moved and renamed class
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 09:18:54 +0000 |
haftmann |
restored naming of lemmas after corresponding constants
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Thu, 21 Dec 2017 18:11:24 +0100 |
nipkow |
tuned op's
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:41 +0000 |
haftmann |
tuned some proofs and added some lemmas
|
file |
diff |
annotate
|
| Fri, 20 Oct 2017 07:46:10 +0200 |
haftmann |
added lemmas and tuned proofs
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|