Wed, 26 Dec 2018 16:25:20 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
Tue, 21 Aug 2018 17:29:46 +0200 |
nipkow |
improved sectioning
|
file |
diff |
annotate
|
Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Fri, 12 Jan 2018 14:08:53 +0100 |
wenzelm |
isabelle update_cartouches -c;
|
file |
diff |
annotate
|
Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
Sat, 19 Dec 2015 11:05:04 +0100 |
haftmann |
abandoned attempt to unify sublocale and interpretation into global theories
|
file |
diff |
annotate
|
Sat, 14 Nov 2015 08:45:52 +0100 |
haftmann |
prefer "rewrites" and "defines" to note rewrite morphisms
|
file |
diff |
annotate
|
Tue, 15 Sep 2015 17:09:13 +0200 |
nipkow |
goali -> i
|
file |
diff |
annotate
|
Wed, 19 Feb 2014 22:05:15 +0100 |
haftmann |
more convenient syntax for permanent interpretation
|
file |
diff |
annotate
|
Wed, 19 Feb 2014 22:05:05 +0100 |
haftmann |
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
|
file |
diff |
annotate
|
Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
file |
diff |
annotate
|
Thu, 23 Jan 2014 16:09:28 +0100 |
nipkow |
installed by Johannes in Extended now
|
file |
diff |
annotate
|
Thu, 23 Jan 2014 16:01:53 +0100 |
nipkow |
hide Fin in output of value via postprocessor; no hinding needed elsewhere
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 16:14:19 +0100 |
nipkow |
tuned names
|
file |
diff |
annotate
|
Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
use case_of_simps
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 16:07:00 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
Wed, 15 May 2013 12:10:39 +0200 |
kuncar |
stronger reflexivity prover
|
file |
diff |
annotate
|
Tue, 14 May 2013 06:54:31 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
Thu, 09 May 2013 03:58:28 +0200 |
nipkow |
standard ivl notation [l,h]
|
file |
diff |
annotate
|
Wed, 08 May 2013 04:16:44 +0200 |
nipkow |
hide Fin on output
|
file |
diff |
annotate
|
Tue, 07 May 2013 10:34:55 +0200 |
nipkow |
tuned name: filter -> constrain (longer but more intuitive)
|
file |
diff |
annotate
|
Tue, 07 May 2013 03:24:23 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Mon, 06 May 2013 15:10:21 +0200 |
nipkow |
improved defns and proofs
|
file |
diff |
annotate
|
Mon, 06 May 2013 00:25:04 +0200 |
nipkow |
simplified proofs
|
file |
diff |
annotate
|
Fri, 03 May 2013 05:25:14 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Fri, 03 May 2013 02:52:25 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Tue, 30 Apr 2013 03:18:07 +0200 |
nipkow |
canonical names of classes
|
file |
diff |
annotate
|
Wed, 17 Apr 2013 21:11:01 +0200 |
nipkow |
complete revision: finally got rid of annoying L-predicate
|
file |
diff |
annotate
|
Mon, 11 Mar 2013 12:27:31 +0100 |
nipkow |
more factorisation of Step & Co
|
file |
diff |
annotate
|
Sun, 10 Mar 2013 18:29:10 +0100 |
nipkow |
factored out Step
|
file |
diff |
annotate
|
Wed, 06 Mar 2013 16:10:56 +0100 |
nipkow |
major redesign: order instead of preorder, new definition of intervals as quotients
|
file |
diff |
annotate
|
Sun, 24 Feb 2013 18:30:35 +0100 |
nipkow |
improved orderings
|
file |
diff |
annotate
|
Fri, 22 Feb 2013 20:12:53 +0100 |
nipkow |
more abstract intervals
|
file |
diff |
annotate
|
Tue, 12 Feb 2013 11:54:29 +0100 |
nipkow |
tuned top
|
file |
diff |
annotate
|
Fri, 25 Jan 2013 16:45:09 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Wed, 26 Sep 2012 03:16:40 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Mon, 17 Sep 2012 02:25:38 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Sun, 16 Sep 2012 11:50:03 +0200 |
nipkow |
converted wt into a set, tuned names
|
file |
diff |
annotate
|
Fri, 07 Sep 2012 07:20:55 +0200 |
nipkow |
adjusted examples
|
file |
diff |
annotate
|
Thu, 19 Apr 2012 20:19:13 +0200 |
nipkow |
added revised version of Abs_Int
|
file |
diff |
annotate
|