simplified method setup;
authorwenzelm
Wed Nov 29 15:44:56 2006 +0100 (2006-11-29)
changeset 215891b02201d7195
parent 21588 cd0dc678a205
child 21590 ef7278f553eb
simplified method setup;
reactivated dead code;
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Nov 29 15:44:51 2006 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Nov 29 15:44:56 2006 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  theory Transitive_Closure
     1.6  imports Inductive
     1.7 -uses ("../Provers/trancl.ML")
     1.8 +uses "~~/src/Provers/trancl.ML"
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -459,8 +459,6 @@
    1.13  
    1.14  subsection {* Setup of transitivity reasoner *}
    1.15  
    1.16 -use "../Provers/trancl.ML";
    1.17 -
    1.18  ML_setup {*
    1.19  
    1.20  structure Trancl_Tac = Trancl_Tac_Fun (
    1.21 @@ -484,7 +482,7 @@
    1.22        | dec _ =  NONE
    1.23      in dec t end;
    1.24  
    1.25 -  end); (* struct *)
    1.26 +  end);
    1.27  
    1.28  change_simpset (fn ss => ss
    1.29    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    1.30 @@ -492,15 +490,13 @@
    1.31  
    1.32  *}
    1.33  
    1.34 -(* Optional methods
    1.35 +(* Optional methods *)
    1.36  
    1.37  method_setup trancl =
    1.38 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
    1.39 +  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
    1.40    {* simple transitivity reasoner *}
    1.41  method_setup rtrancl =
    1.42 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
    1.43 +  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
    1.44    {* simple transitivity reasoner *}
    1.45  
    1.46 -*)
    1.47 -
    1.48  end