| 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
|