Cheat support equations in new parser
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 03 May 2010 11:43:08 +0200
changeset 2020 8468be06bff1
parent 2019 0a04acc91ca1
child 2021 f761f83e541a
Cheat support equations in new parser
Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 03 11:37:44 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 11:43:08 2010 +0200
@@ -508,11 +508,12 @@
   val lthy22 = Class.prove_instantiation_instance tac lthy21
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
-(*  val _ = warning "Support Equations";
-  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
-  val lthy23 = note_suffix "supp" q_supp lthy22;*)
+  val _ = warning "Support Equations";
+  (*supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1*)
+  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => Skip_Proof.cheat_tac thy)) handle _ => [];
+  val lthy23 = note_suffix "supp" q_supp lthy22;
 in
-  (0, lthy22)
+  (0, lthy23)
 end
 *}