# HG changeset patch
# User wenzelm
# Date 1164811496 -3600
# Node ID 1b02201d71952caf82cb255cfbecee4fdfc653d4
# Parent  cd0dc678a2055f8f0018c20e85386be9c3fa6c36
simplified method setup;
reactivated dead code;

diff -r cd0dc678a205 -r 1b02201d7195 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Nov 29 15:44:51 2006 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 29 15:44:56 2006 +0100
@@ -8,7 +8,7 @@
 
 theory Transitive_Closure
 imports Inductive
-uses ("../Provers/trancl.ML")
+uses "~~/src/Provers/trancl.ML"
 begin
 
 text {*
@@ -459,8 +459,6 @@
 
 subsection {* Setup of transitivity reasoner *}
 
-use "../Provers/trancl.ML";
-
 ML_setup {*
 
 structure Trancl_Tac = Trancl_Tac_Fun (
@@ -484,7 +482,7 @@
       | dec _ =  NONE
     in dec t end;
 
-  end); (* struct *)
+  end);
 
 change_simpset (fn ss => ss
   addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
@@ -492,15 +490,13 @@
 
 *}
 
-(* Optional methods
+(* Optional methods *)
 
 method_setup trancl =
-  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
+  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
   {* simple transitivity reasoner *}
 method_setup rtrancl =
-  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
+  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   {* simple transitivity reasoner *}
 
-*)
-
 end