| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 13:39:34 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 19:20:11 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 21:07:57 +0100 |
wenzelm |
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 14:21:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Tue, 23 Jul 2013 16:56:46 +0200 |
krauss |
eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates
|
file |
diff |
annotate
|
| Sun, 29 Apr 2012 01:17:25 +0200 |
krauss |
dependency graphs: fixed direction of edges
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:26:30 +0900 |
griff |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 21:41:01 +0100 |
krauss |
tuned headers
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:40 +0200 |
krauss |
discontinued continuations to simplify control flow; dropped optimization in scnp
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:38 +0200 |
krauss |
use Cache structure instead of passing tables around explicitly
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:54 +0200 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Thu, 10 Jun 2010 12:24:03 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| Tue, 08 Jun 2010 16:37:19 +0200 |
haftmann |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 21:56:55 +0100 |
wenzelm |
just one copy of structure Term_Graph (in Pure);
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:57:08 +0100 |
wenzelm |
clarified @{const_name} vs. @{const_abbrev};
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:04 +0100 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn 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
|
| Sun, 03 Jan 2010 15:08:17 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
new year's resolution: reindented code in function package
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
simplified
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
file |
diff |
annotate
|
| Mon, 23 Nov 2009 15:05:59 +0100 |
krauss |
eliminated dead code and some unused bindings, reported by polyml
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:22:10 +0200 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 07:38:03 +0200 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 09:07:49 +0200 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 14:20:32 +0200 |
haftmann |
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|