isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

new Brouwer ordinal example
2005-05-25, by paulson
more cleanup
2005-05-25, by kleing
tuned thm_style section
2005-05-25, by kleing
added ? explanations
2005-05-25, by nipkow
renamed search criterion 'rewrite' to 'simp'
2005-05-25, by kleing
SML/NJ compatibility
2005-05-25, by paulson
new environments for Proof General notes
2005-05-25, by paulson
removed obsolete findI, findE, findEs
2005-05-25, by kleing
removed LICENCE note -- everything is subject to Isabelle licence as
2005-05-25, by wenzelm
*** empty log message ***
2005-05-25, by nipkow
grammar
2005-05-25, by nipkow
shorted proof that lift is chfin
2005-05-25, by huffman
Removed shell variables. Now uses isatool getenv -b SPASS_HOME.
2005-05-25, by quigley
Generic version of spassshell. Add SPASS_HOME to .bashrc so that shell script can find it.
2005-05-24, by quigley
ML_idf antiquotation
2005-05-24, by haftmann
oracle example converted to Isar
2005-05-24, by paulson
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
2005-05-24, by paulson
A new structure and reduced indentation
2005-05-24, by paulson
Simplified version of strict sum theory, using TypedefPcpo
2005-05-24, by huffman
Simplified version of strict product theory, using TypedefPcpo
2005-05-24, by huffman
New theory for defining subtypes of pcpos
2005-05-24, by huffman
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
2005-05-24, by huffman
Moved admissibility definitions and lemmas to a separate theory
2005-05-24, by huffman
moved continuity simproc to Cfun.thy
2005-05-23, by huffman
moved continuity simproc to Cont.thy
2005-05-23, by huffman
moved theorem cont2cont_CF1L_rev2 to Cont.thy
2005-05-23, by huffman
tuned setsum rewrites
2005-05-23, by nipkow
* Pure/Syntax: In schematic variable names, *any* symbol following
2005-05-23, by wenzelm
interpreters for lfp/gfp added
2005-05-23, by webertj
obsolete;
2005-05-23, by wenzelm
spassshell and testout.py are used to filter the proof part out of SPASS's
2005-05-23, by quigley
tuned pretty_sg;
2005-05-23, by wenzelm
node_trans: revert to original transaction code (pre 1.54);
2005-05-23, by wenzelm
use: not a theory command!
2005-05-23, by wenzelm
converted back from 0..< to <.
2005-05-23, by nipkow
added email
2005-05-23, by haftmann
tuned trace info (depth)
2005-05-23, by nipkow
simplifier trace info; Suc-intervals
2005-05-23, by nipkow
some adaptions
2005-05-23, by haftmann
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
2005-05-23, by quigley
tuned;
2005-05-22, by wenzelm
string FindTheorems.criterion;
2005-05-22, by wenzelm
added read_criterion/pretty_criterion;
2005-05-22, by wenzelm
added show_dummy_patterns;
2005-05-22, by wenzelm
updated;
2005-05-22, by wenzelm
Retrieve theorems from proof context -- improved version of
2005-05-22, by wenzelm
added Pure/simplifier.ML, Pure/Isar/find_theorems.ML;
2005-05-22, by wenzelm
moved everything related to thms_containing to find_theorems.ML;
2005-05-22, by wenzelm
added reserved;
2005-05-22, by wenzelm
added ident_with;
2005-05-22, by wenzelm
fold ProofContext.declare_term;
2005-05-22, by wenzelm
added 'print_simpset';
2005-05-22, by wenzelm
added print_simpset;
2005-05-22, by wenzelm
added find_theorems.ML, ../simplifier.ML;
2005-05-22, by wenzelm
tuned terms_of_tpairs;
2005-05-22, by wenzelm
added string_of_thmref, selections, fact_index_of, valid_thms;
2005-05-22, by wenzelm
FindTheorems.print_theorems;
2005-05-22, by wenzelm
findI/Es/E: adapted to FindTheorems.find_XXX, results use thmref instead of string;
2005-05-22, by wenzelm
major tuning;
2005-05-22, by wenzelm
Simplifier already setup in Pure;
2005-05-22, by wenzelm

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle