Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/blastdata.ML
author paulson
Tue, 11 Oct 2005 15:03:36 +0200
changeset 17828 c82fb51ee18d
parent 16774 515b6020cf5d
child 18171 c4f873d65603
permissions -rw-r--r--
simplifying the treatment of nameless theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset 
     1
 












4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




     2


(*** Applying BlastFun to create Blast_tac ***)













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




     3


structure Blast_Data = 













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




     4


  struct













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




     5


  type claset	= Cla.claset








16774






515b6020cf5d
experimental code to reduce the amount of type information in blast



paulson


parents: 
11748

diff
changeset




     6


  val is_hol    = false








7355






4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




     7


  val notE	= notE













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




     8


  val ccontr	= ccontr













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




     9


  val contr_tac = Cla.contr_tac













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    10


  val dup_intr	= Cla.dup_intr













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    11


  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    12


  val claset	= Cla.claset













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    13


  val rep_cs    = Cla.rep_cs













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    14


  val cla_modifiers = Cla.cla_modifiers;













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    15


  val cla_meth' = Cla.cla_meth'













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    16


  end;













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    17














4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    18


structure Blast = BlastFun(Blast_Data);













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    19














4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    20


val Blast_tac = Blast.Blast_tac













4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;



wenzelm


parents: 

diff
changeset




    21


and blast_tac = Blast.blast_tac;















isabelle