# HG changeset patch # User Christian Urban # Date 1259263116 -3600 # Node ID 646bfe5905b3bafaa09f6464020d5ef72bdf32e3 # Parent fafcc54e531d030ba4a1f50b6d2ae7d20a9d9005 tuned comments diff -r fafcc54e531d -r 646bfe5905b3 FSet.thy --- a/FSet.thy Thu Nov 26 19:51:31 2009 +0100 +++ b/FSet.thy Thu Nov 26 20:18:36 2009 +0100 @@ -351,6 +351,53 @@ apply(rule cheat) prefer 2 apply(rule cheat) +apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*}) +thm RES_FORALL_RSP +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) +apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*}) quotient_def diff -r fafcc54e531d -r 646bfe5905b3 QuotMain.thy --- a/QuotMain.thy Thu Nov 26 19:51:31 2009 +0100 +++ b/QuotMain.thy Thu Nov 26 20:18:36 2009 +0100 @@ -885,11 +885,8 @@ -(****************************************) -(* cleaning of the theorem *) -(****************************************) - +section {* Cleaning of the theorem *} (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \ bool) to (int 'b quo \ bool) *) ML {* diff -r fafcc54e531d -r 646bfe5905b3 UnusedQuotMain.thy --- a/UnusedQuotMain.thy Thu Nov 26 19:51:31 2009 +0100 +++ b/UnusedQuotMain.thy Thu Nov 26 20:18:36 2009 +0100 @@ -484,7 +484,7 @@ ML {* atomize_goal @{theory} @{term "x memb [] = False"} *} -ML {* atomize_goal @{theory} @{term "x = xa ⟹ a # x = a # xa"} *} +ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}