| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 22:19:14 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Tue, 02 Jun 2015 09:40:04 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:43:03 +0100 |
wenzelm |
local fixes may depend on goal params;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:52:57 +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 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 21:11:03 +0200 |
blanchet |
fixed some spelling mistakes
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:16:54 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 19:58:33 +0100 |
wenzelm |
more standard method_setup;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:43:29 +0100 |
wenzelm |
more rigid type_name demands, based on educated guesses about the tools involved here;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
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
|
| Wed, 10 Apr 2013 12:24:43 +0200 |
wenzelm |
proper proof context;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:00:34 +0100 |
wenzelm |
prefer explicitly qualified exception List.Empty;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 16:27:47 +0200 |
wenzelm |
modernized structure Rule_Insts;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 15:07:29 +0100 |
wenzelm |
avoid catch-all exception handler, presumably TERM was meant here;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 14:55:25 +0100 |
wenzelm |
tuned -- eliminated Sign.intern_sort;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:06:43 +0100 |
wenzelm |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 00:08:56 +0100 |
wenzelm |
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 23:25:04 +0200 |
wenzelm |
eliminated THENL -- use THEN RANGE;
|
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
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 11:46:47 +0200 |
wenzelm |
handle _ should be avoided (spurious Interrupt will spoil the game);
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:39 +0200 |
wenzelm |
pervasive RuleInsts;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 23:12:54 +0200 |
wenzelm |
use regular error function;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:44 +0100 |
wenzelm |
simplified get_thm(s): back to plain name argument;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:28:08 +0100 |
wenzelm |
auxiliary dynamic_thm(s) for fact lookup;
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 18:30:02 +0200 |
urbanc |
some cleaning up
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:22:51 +0200 |
wenzelm |
avoid low-level tsig;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 11:16:24 +0200 |
narboux |
generate_fresh works even if there is no free variable in the goal
|
file |
diff |
annotate
|
| Thu, 24 May 2007 14:04:06 +0200 |
narboux |
fix a bug : the semantics of no_asm was the opposite
|
file |
diff |
annotate
|
| Thu, 24 May 2007 12:00:47 +0200 |
narboux |
add an option in fresh_fun_simp to prevent rewriting in assumptions
|
file |
diff |
annotate
|
| Mon, 21 May 2007 19:14:12 +0200 |
narboux |
search bottom up to get the inner fresh fun
|
file |
diff |
annotate
|
| Mon, 21 May 2007 16:19:56 +0200 |
narboux |
change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
|
file |
diff |
annotate
|
| Wed, 25 Apr 2007 15:38:56 +0200 |
narboux |
fix sml compilation
|
file |
diff |
annotate
|
| Tue, 24 Apr 2007 18:06:04 +0200 |
narboux |
update fresh_fun_simp for debugging purposes
|
file |
diff |
annotate
|
| Tue, 24 Apr 2007 14:01:23 +0200 |
narboux |
adds op in front of an infix to fix SML compilation
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 14:30:35 +0200 |
narboux |
modify fresh_fun_simp to ease debugging
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 16:27:53 +0200 |
narboux |
add a tactic to generate fresh names
|
file |
diff |
annotate
|