# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260290031 -3600
# Node ID b029f242d85d544147fc5247bbe7e5d986df3973
# Parent  520a4084d064450c18ec3359773ada0fc4fd4d24
chnaged syntax to "lifting theorem"

diff -r 520a4084d064 -r b029f242d85d Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 17:30:00 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 17:33:51 2009 +0100
@@ -141,7 +141,7 @@
 done
 
 lemma "PLUS a b = PLUS a b"
-apply(lifting_setup rule: test1)
+apply(lifting_setup test1)
 apply(regularize)
 apply(injection)
 apply(cleaning)
@@ -203,7 +203,7 @@
 done
 
 lemma "foldl PLUS x [] = x"
-apply(lifting rule: ho_tst)
+apply(lifting ho_tst)
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
@@ -343,7 +343,7 @@
 done
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
-apply(lifting rule: lam_tst4)
+apply(lifting lam_tst4)
 apply(cleaning)
 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric])
diff -r 520a4084d064 -r b029f242d85d Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 17:30:00 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:33:51 2009 +0100
@@ -1188,8 +1188,6 @@
 
 (* methods / interface *)
 ML {*
-val rule_spec =  Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm
-
 (* FIXME: if the argument order changes then this can be just one function *)
 fun mk_method1 tac thm ctxt =
   SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) 
@@ -1199,11 +1197,11 @@
 *}
 
 method_setup lifting =
-  {* rule_spec >> (mk_method1 lift_tac) *}
+  {* Attrib.thm >> (mk_method1 lift_tac) *}
   {* Lifting of theorems to quotient types. *}
 
 method_setup lifting_setup =
-  {* rule_spec >> (mk_method1 procedure_tac) *}
+  {* Attrib.thm >> (mk_method1 procedure_tac) *}
   {* Sets up the three goals for the lifting procedure. *}
 
 method_setup regularize =