Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
handle cgoal;
authorwenzelm
Tue, 13 Jul 1999 13:54:08 +0200
changeset 6996 1a28d968c5aa
parent 6995 d824a86266a9
child 6997 1833bdd83ebf
handle cgoal;
src/Pure/Isar/local_defs.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/local_defs.ML	Tue Jul 13 13:53:34 1999 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Jul 13 13:54:08 1999 +0200
@@ -17,7 +17,7 @@
 struct
 
 
-val refl_tac = Tactic.rtac Drule.reflexive_thm;
+val refl_tac = Tactic.rtac (standard (Drule.reflexive_thm RS Drule.triv_goal));
 
 
 fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
--- a/src/Pure/Isar/proof.ML	Tue Jul 13 13:53:34 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 13 13:54:08 1999 +0200
@@ -388,7 +388,7 @@
 fun export_wrt inner opt_outer =
   let
     val (fixes, asms) = diff_context inner opt_outer;
-    val casms = map #1 asms;
+    val casms = map (Drule.mk_cgoal o #1) asms;
     val tacs = map #2 asms;
   in (export fixes casms, tacs) end;
 
@@ -449,7 +449,7 @@
     val tsig = Sign.tsig_of sign;
 
     val casms = map #1 (assumptions state);
-    val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
+    val bad_hyps = Library.gen_rems Term.aconv (hyps, map (Thm.term_of o Drule.mk_cgoal) casms);
   in
     if not (null bad_hyps) then
       err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
@@ -538,10 +538,13 @@
 val assm = gen_assume ProofContext.assume;
 val assm_i = gen_assume ProofContext.assume_i;
 
-val assume = assm (assume_tac, K all_tac);
-val assume_i = assm_i (assume_tac, K all_tac);
-val presume = assm (K all_tac, K all_tac);
-val presume_i = assm_i (K all_tac, K all_tac);
+val hard_asm_tac = Tactic.etac Drule.triv_goal;
+val soft_asm_tac = Tactic.rtac Drule.triv_goal;
+
+val assume = assm (hard_asm_tac, soft_asm_tac);
+val assume_i = assm_i (hard_asm_tac, soft_asm_tac);
+val presume = assm (soft_asm_tac, soft_asm_tac);
+val presume_i = assm_i (soft_asm_tac, soft_asm_tac);
 
 
 
@@ -581,7 +584,7 @@
     val casms = map #1 (assumptions state');
 
     val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
-    fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Thm.assume casm COMP revcut_rl) RS thm);
+    fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm);
     val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
   in
     state'
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 13 13:53:34 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 13 13:54:08 1999 +0200
@@ -660,7 +660,7 @@
 
     val cprops = map (Thm.cterm_of sign) props;
     val cprops_tac = map (rpair tac) cprops;
-    val asms = map (Drule.forall_elim_vars (maxidx + 1) o Thm.assume) cprops;
+    val asms = map (Drule.forall_elim_vars (maxidx + 1) o Drule.assume_goal) cprops;
 
     val ths = map (fn th => ([th], [])) asms;
     val (ctxt'', (_, thms)) =
isabelle