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/ZF/Main.ML
author wenzelm
Mon, 20 Jun 2005 22:14:08 +0200
changeset 16494 6961e8ab33e1
parent 12725 7ede865e1fe5
child 17876 b9c92f384109
permissions -rw-r--r--
added certify_prop, cert_term, cert_prop;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12425
97975229f893 added Main.ML;
wenzelm
parents:
diff changeset 
     1
 












97975229f893
added Main.ML;



wenzelm


parents: 

diff
changeset




     2


structure Main =













97975229f893
added Main.ML;



wenzelm


parents: 

diff
changeset




     3


struct













97975229f893
added Main.ML;



wenzelm


parents: 

diff
changeset




     4


  val thy = the_context ();













97975229f893
added Main.ML;



wenzelm


parents: 

diff
changeset




     5


end;








12715






f7299128cd7d
moved setmksimps to Main!



wenzelm


parents: 
12425

diff
changeset




     6









12725






7ede865e1fe5
renamed forall_elim_vars_safe to gen_all;



wenzelm


parents: 
12720

diff
changeset




     7


simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);















isabelle