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
|