| Wed, 22 Apr 2015 12:11:48 +0200 |
nipkow |
added simp rules for ==>
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:33:25 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 21:31:58 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 15:48:02 +0100 |
wenzelm |
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 11:40:59 +0100 |
nipkow |
merged
|
file |
diff |
annotate
| base
|
| Fri, 30 Oct 2009 13:59:49 +0100 |
haftmann |
moved Commutative_Ring into session Decision_Procs
|
file |
diff |
annotate
| base
|