Sat, 29 Jul 2006 00:51:34 +0200 tuned comment;
wenzelm [Sat, 29 Jul 2006 00:51:34 +0200] rev 20252
tuned comment;
Sat, 29 Jul 2006 00:51:33 +0200 added add_fixes_direct;
wenzelm [Sat, 29 Jul 2006 00:51:33 +0200] rev 20251
added add_fixes_direct; tuned;
Sat, 29 Jul 2006 00:51:32 +0200 prove: proper assumption context, more tactic arguments;
wenzelm [Sat, 29 Jul 2006 00:51:32 +0200] rev 20250
prove: proper assumption context, more tactic arguments; tuned;
Sat, 29 Jul 2006 00:51:31 +0200 added mk_conjunction_list;
wenzelm [Sat, 29 Jul 2006 00:51:31 +0200] rev 20249
added mk_conjunction_list;
Sat, 29 Jul 2006 00:51:29 +0200 Goal.prove: more tactic arguments;
wenzelm [Sat, 29 Jul 2006 00:51:29 +0200] rev 20248
Goal.prove: more tactic arguments;
Fri, 28 Jul 2006 18:37:25 +0200 Checking for unsound proofs. Tidying.
paulson [Fri, 28 Jul 2006 18:37:25 +0200] rev 20247
Checking for unsound proofs. Tidying.
Fri, 28 Jul 2006 18:36:24 +0200 "all theorems" mode forces definition-expansion off.
paulson [Fri, 28 Jul 2006 18:36:24 +0200] rev 20246
"all theorems" mode forces definition-expansion off. signature tidying
Fri, 28 Jul 2006 18:11:22 +0200 title fixed
webertj [Fri, 28 Jul 2006 18:11:22 +0200] rev 20245
title fixed
Thu, 27 Jul 2006 23:28:30 +0200 replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm [Thu, 27 Jul 2006 23:28:30 +0200] rev 20244
replaced extern_skolem by slightly more simplistic revert_skolems; moved fix_frees to variable.ML;
Thu, 27 Jul 2006 23:28:28 +0200 renamed ProofContext.fix_frees to Variable.fix_frees;
wenzelm [Thu, 27 Jul 2006 23:28:28 +0200] rev 20243
renamed ProofContext.fix_frees to Variable.fix_frees;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip