# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255854893 -7200
# Node ID 89283c1dbba7e1df4c8fb95809f4121e9ef93fd4
# Parent  6ddb2f99be1d81fd592818f143d483f4bd721ea8
Test if we can already do sth with the transformed theorem.

diff -r 6ddb2f99be1d -r 89283c1dbba7 QuotMain.thy
--- a/QuotMain.thy	Sun Oct 18 08:44:16 2009 +0200
+++ b/QuotMain.thy	Sun Oct 18 10:34:53 2009 +0200
@@ -1167,11 +1167,13 @@
   done
 
 ML {* val thm = @{thm list_induct_r} OF [li] *}
-ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
+ML {* val trm_r = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
 
-prove trm
+ML {* val trm = build_goal_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
+
+prove list_induct_tr: trm_r
 apply (atomize(full))
 apply (simp only: id_def[symmetric])
 
@@ -1300,6 +1302,13 @@
 apply (simp)
 sorry
 
+prove list_induct_t: trm
+apply (simp only: list_induct_tr[symmetric])
+apply (tactic {* rtac thm 1 *})
+done
+
+ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *}
+
 thm list.recs(2)