973 

   973 

   974 lemma trueprop_cong:

   974 lemma trueprop_cong:

   975   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"

   975   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"

   976   by auto

   976   by auto

   977 

   977 

   978 

   981 

   979 thm QUOT_TYPE_I_fset.R_trans2

   982 thm QUOT_TYPE_I_fset.R_trans2

   980 ML {*

   983 ML {*

   981   fun foo_tac' ctxt =

   984   fun foo_tac' ctxt =

   982     REPEAT_ALL_NEW (FIRST' [

   985     REPEAT_ALL_NEW (FIRST' [

   985       rtac @{thm cons_preserves},

   988       rtac @{thm cons_preserves},

   986       rtac @{thm mem_respects},

   989       rtac @{thm mem_respects},

   987       rtac @{thm card1_rsp},

   990       rtac @{thm card1_rsp},

   988       rtac @{thm QUOT_TYPE_I_fset.R_trans2},

   991       rtac @{thm QUOT_TYPE_I_fset.R_trans2},

   989       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),

   992       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),

   991       rtac @{thm ext},

   994       rtac @{thm ext},

   992 (*      rtac @{thm eq_reflection},*)

   995 (*      rtac @{thm eq_reflection},*)

   993       CHANGED o (ObjectLogic.full_atomize_tac)

   996       CHANGED o (ObjectLogic.full_atomize_tac)

   994     ])

   997     ])

   995 *}

   998 *}

  1230 | OBJ1 "(string * (string \<Rightarrow> obj1)) list"

  1233 | OBJ1 "(string * (string \<Rightarrow> obj1)) list"

  1231 | INVOKE1 "obj1 \<Rightarrow> string"

  1234 | INVOKE1 "obj1 \<Rightarrow> string"

  1232 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"

  1235 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"

  1233 *)

  1236 *)

  1234 

  1237