Mercurial Mercurial > repos > Old_HOL / 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.
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
authornipkow
Wed, 31 Aug 1994 17:50:59 +0200
changeset 133 4a2bb4fbc168
parent 132 47be9d22a0d6
child 134 4b7da5a895e7
Added IMP, which necessiated changes in intr_elim.tex (mk_cases). Improved layout for set comprehension in Set.thy.
Makefile file | annotate | diff | comparison | revisions
Set.thy file | annotate | diff | comparison | revisions
intr_elim.ML file | annotate | diff | comparison | revisions 
--- a/Makefile	Wed Aug 31 16:25:19 1994 +0200
+++ b/Makefile	Wed Aug 31 17:50:59 1994 +0200
@@ -31,6 +31,9 @@
 	../Provers/classical.ML ../Provers/simplifier.ML \
 	../Provers/splitter.ML ../Provers/ind.ML
 
+IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
+            IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy
+
 EX_FILES = ex/ROOT.ML ex/cla.ML \
 	   ex/LexProd.ML ex/LexProd.thy ex/meson.ML ex/mesontest.ML\
 	   ex/MT.ML ex/MT.thy ex/Acc.ML ex/Acc.thy \
@@ -64,13 +67,13 @@
 $(BIN)/Pure:
 	cd ../Pure;  $(MAKE)
 
-#Directory Subst also tests the system
+#Directories IMP and Subst also test the system
 #Load ex/ROOT.ML last since it creates the file "test"
-test:   $(BIN)/HOL  $(SUBST_FILES)  $(EX_FILES)
+test:   $(BIN)/HOL  $(IMP_FILES) $(SUBST_FILES)  $(EX_FILES)
 	case "$(COMP)" in \
-	poly*)	echo 'use"Subst/ROOT.ML"; use"ex/ROOT.ML"; quit();' \
+	poly*)	echo 'use"IMP/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML"; quit();' \
                         | $(COMP) $(BIN)/HOL ;;\
-	sml*)	echo 'use"Subst/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/HOL;;\
+	sml*)	echo 'use"IMP/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/HOL;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
--- a/Set.thy	Wed Aug 31 16:25:19 1994 +0200
+++ b/Set.thy	Wed Aug 31 17:50:59 1994 +0200
@@ -46,7 +46,7 @@
   (** Binding Constants **)
 
   "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")
-  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("{_ |/_./ _}")
+  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
 
   (* Big Intersection / Union *)
 
--- a/intr_elim.ML	Wed Aug 31 16:25:19 1994 +0200
+++ b/intr_elim.ML	Wed Aug 31 17:50:59 1994 +0200
@@ -113,9 +113,19 @@
 
 (*Applies freeness of the given constructors, which *must* be unfolded by
   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
-  for inference systems. *)
+  for inference systems.
 fun con_elim_tac defs =
     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
+ *)
+fun con_elim_tac simps =
+  let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs))
+  in ALLGOALS(EVERY'[elim_tac,
+                     asm_full_simp_tac (nat_ss addsimps simps),
+                     elim_tac,
+                     REPEAT o bound_hyp_subst_tac])
+     THEN prune_params_tac
+  end;
+
 
 (*String s should have the form t:Si where Si is an inductive set*)
 fun mk_cases defs s =
Old_HOL