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.
ObtainFun;
authorwenzelm
Wed, 05 Jan 2000 11:50:55 +0100
changeset 8099 6a087be9f6d9
parent 8098 a7ee88ef2fa5
child 8100 6186ee807f2e
ObtainFun;
src/FOL/cladata.ML file | annotate | diff | comparison | revisions
src/HOL/cladata.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/cladata.ML	Wed Jan 05 11:50:13 2000 +0100
+++ b/src/FOL/cladata.ML	Wed Jan 05 11:50:55 2000 +0100
@@ -20,8 +20,8 @@
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Cla;
-open BasicClassical;
+structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
+structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
 
 
 (*Better for fast_tac: needs no quantifier duplication!*)
--- a/src/HOL/cladata.ML	Wed Jan 05 11:50:13 2000 +0100
+++ b/src/HOL/cladata.ML	Wed Jan 05 11:50:55 2000 +0100
@@ -40,8 +40,8 @@
   end;
 
 structure Classical = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Classical;
-open BasicClassical;
+structure BasicClassical: BASIC_CLASSICAL = Classical; open BasicClassical;
+structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
 
 (*Propositional rules*)
 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
isabelle