isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

examples now use ~= for "not equals"
1993-10-07, by lcp
ifol.thy: added ~= for "not equals"
1993-10-07, by lcp
changed filenames to lower case name of theory the file contains
1993-10-06, by clasohm
rename list-fn to listfn
1993-10-06, by clasohm
changed "list-fn" to "listfn"
1993-10-06, by clasohm
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
1993-10-06, by lcp
Retrying yet again after network problems
1993-10-06, by lcp
Modification of examples for the new operators, < and le.
1993-10-05, by lcp
Retry of the previous commit (network outage)
1993-10-05, by lcp
Retry of the previous commit (network outage)
1993-10-05, by lcp
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
1993-10-05, by lcp
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
1993-10-05, by lcp
added functions that operate on filenames: split_filename (originally located
1993-10-05, by clasohm
replaced id by idt;
1993-10-04, by wenzelm
added parse rules for -> and *;
1993-10-04, by wenzelm
replaced id by idt;
1993-10-04, by wenzelm
Pure/Thy/syntax.ML
1993-10-04, by wenzelm
Pure/ROOT.ML
1993-10-04, by wenzelm
lots of internal cleaning and tuning;
1993-10-04, by wenzelm
asm_full_simp_tac now fails when applied to a state w/o subgoals.
1993-10-01, by nipkow
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-30, by lcp
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-30, by lcp
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-30, by lcp
Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10
1993-09-24, by lcp
Added ex_ex1I: new introduction rule for the EX! quantifier.
1993-09-24, by lcp
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
1993-09-24, by lcp
This commit should not have been necessary. For some reason, the previous
1993-09-21, by lcp
make-all now has set +e so that New Jersey runs will continue even if some
1993-09-20, by lcp
Installation of new simplfier. Previously appeared to set up the old
1993-09-20, by lcp
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
1993-09-17, by lcp
Installation of new simplifier for ZF. Deleted all congruence rules not
1993-09-17, by lcp
test commit
1993-09-17, by lcp
added header
1993-09-16, by nipkow
defined local addcongs
1993-09-16, by nipkow
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
1993-09-16, by clasohm
changed addcongs to addeqcongs in simplifier.ML
1993-09-16, by nipkow
Initial revision
1993-09-16, by clasohm

less more | (0) +120 +1000 +3000 +10000 +30000 tip

isabelle