| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 23:14:06 +0100 |
blanchet |
effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 01:29:50 +0100 |
blanchet |
optimized 'bad apple' method calls
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Thu, 01 Aug 2013 00:18:45 +0200 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| Tue, 28 May 2013 13:19:51 +0200 |
popescua |
merged Well_Order_Extension into Zorn
|
file |
diff |
annotate
|
| Fri, 24 May 2013 19:09:56 +0200 |
popescua |
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
|
file |
diff |
annotate
|
| Fri, 24 May 2013 17:37:06 +0200 |
popescua |
modernized Zorn (by Christian Sternagel)
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 21:48:03 +0100 |
wenzelm |
prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 13:33:54 +0200 |
blanchet |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 22:26:55 +0100 |
haftmann |
tuned specifications
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 19:34:52 +0100 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 20:03:13 +0100 |
wenzelm |
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 10:30:36 -0800 |
huffman |
fix more looping simp rules
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 19:02:33 +0200 |
huffman |
fixed extremely slow proof of Chain_inits_DiffI
|
file |
diff |
annotate
|
| Tue, 03 Jun 2008 12:38:39 +0200 |
ballarin |
Tuned proof.
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:57:19 +0200 |
berghofe |
Adapted to encoding of sets as predicates
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 16:47:45 +0100 |
nipkow |
reorganization
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 11:42:46 +0100 |
nipkow |
More defns and thms
|
file |
diff |
annotate
|
| Fri, 14 Mar 2008 19:57:32 +0100 |
nipkow |
Added Order_Relation
|
file |
diff |
annotate
|
| Sun, 02 Mar 2008 15:02:06 +0100 |
nipkow |
Generalized Zorn and added well-ordering theorem
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 14:37:00 +0100 |
haftmann |
switched from PreList to ATP_Linkup
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:09 +0100 |
haftmann |
switched import from Main to PreList
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:28:13 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|