isabelle: Graph

expandshort
1993-11-18, by lcp
Misc modifs such as expandshort
1993-11-18, by lcp
added loaded_thys to signature and removed list_/set_loaded
1993-11-16, by clasohm
changed use_thy's parameter to exact theory name
1993-11-16, by clasohm
made pseudo theories for all ML files;
1993-11-16, by clasohm
moved call of store_theory to end of use t.thy; use t.ML;
1993-11-16, by clasohm
replaced \un by \union in "Simplification sets"
1993-11-16, by clasohm
changed use_thy's parameter to exact theory name
1993-11-16, by clasohm
changed all co- and co_ to co
1993-11-15, by lcp
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
1993-11-15, by lcp
Added commentary
1993-11-15, by lcp
fun parents: removed pp block (didn't have any effect)
1993-11-15, by wenzelm
changed application format for pretty-printer
1993-11-14, by nipkow
Misc updates
1993-11-12, by lcp
Misc updates
1993-11-12, by lcp
changed formatting for application
1993-11-11, by nipkow
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
1993-11-11, by nipkow
Various updates for Isabelle-93
1993-11-11, by lcp
new style file
1993-11-11, by lcp
adapted "Defining theories" to new use_thy
1993-11-11, by clasohm
replaced by current version;
1993-11-11, by wenzelm
replaced by current version;
1993-11-11, by wenzelm
*** empty log message ***
1993-11-11, by wenzelm
Initial revision
1993-11-10, by lcp
Initial revision
1993-11-10, by lcp
Initial revision
1993-11-09, by lcp
Target "test" now depends on examples files
1993-11-09, by lcp
Target "test" now depends on examples files
1993-11-09, by lcp
fixed a bug in POLY.ML: delete_file didn't close streams;
1993-11-09, by clasohm
renamed hard-quant.ML to hardquant.ML
1993-11-09, by clasohm
renamed int-prover.ML to intprover.ML,
1993-11-09, by clasohm
renamed int-prover.ML to intprover.ML,
1993-11-09, by clasohm
now forbids semicolons in the body of br, etc. No longer
1993-11-09, by lcp
Minor changes; addition of counit.ML
1993-11-08, by lcp
change of my address
1993-11-05, by nipkow
Added documenation of change_simp.
1993-11-05, by lcp
renamed co_inductive.ML to coinductive.ML
1993-11-04, by clasohm
renamed twos-compl.ML to twos_compl.ML
1993-11-04, by clasohm
renamed some files
1993-11-04, by clasohm
commented out install_pp for term, typ
1993-11-04, by wenzelm
added infix delsimps
1993-10-29, by nipkow
added function del_simps
1993-10-29, by nipkow
deletion of obsolete/private files; update of README
1993-10-28, by lcp
minor changes e.g. datatype_elims
1993-10-28, by lcp
now uses datatype_intrs and datatype_elims
1993-10-28, by lcp
updated version to October 93
1993-10-28, by lcp
no longer specifies "-h 15000". Instead $ISABELLECOMP should
1993-10-27, by lcp
corrected some spelling mistakes;
1993-10-26, by clasohm
added white-space;
1993-10-25, by wenzelm
added white-space;
1993-10-25, by wenzelm
removed a bug that occured when a path was specified for use_thy's parameter
1993-10-22, by clasohm
ZF/ex/tf,tf_fn: renamed the variable tf to f everywhere
1993-10-22, by lcp
renamed some files
1993-10-22, by clasohm
added -h 15000 for Poly/ML in Makefile,
1993-10-22, by clasohm
changes in Readthy:
1993-10-22, by clasohm
delete_file now has type string -> unit in both NJ and POLY,
1993-10-22, by clasohm
changes for new Readthy
1993-10-22, by clasohm
sample datatype defs now use datatype_intrs, datatype_elims
1993-10-22, by lcp
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
1993-10-22, by lcp
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
1993-10-22, by lcp
goals/print_top,prepare_proof: now call \!print_goals_ref
1993-10-22, by lcp
Pure/drule/print_goals_ref: new, for Centaur interface
1993-10-21, by lcp
/NJ,POLY/delete_file: new
1993-10-21, by lcp
simpdata/basify: now calls new fastype_of
1993-10-21, by lcp
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
1993-10-21, by lcp
now calls new fastype_of in three places
1993-10-21, by lcp
Pure/Syntax/printer/is_prop: now calls fastype_of1
1993-10-21, by lcp
Pure/term/fastype_of1: renamed from fastype_of
1993-10-21, by lcp
renamed: S4.thy to s4.thy, S43.thy to s43.thy, T.thy to t.thy
1993-10-17, by clasohm
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
1993-10-17, by clasohm
file_info now returns a string that does not contain the path/filename
1993-10-15, by clasohm
added parser.ML, install_pp.ML
1993-10-15, by wenzelm
ZF/ex/tf/tree,forest_unfold: streamlined the proofs
1993-10-15, by lcp
ZF/ind-syntax/refl_thin: new
1993-10-15, by lcp
classical/swap_res_tac: recoded to allow backtracking
1993-10-15, by lcp
Added gen_all to simpdata.ML.
1993-10-12, by nipkow
renamed ordinal.thy to ord.thy
1993-10-11, by clasohm
renamed ordinal.ML to ord.ML
1993-10-11, by clasohm
renamed ordinal.* to ord.*
1993-10-11, by clasohm
"The" now a binder, removed translation;
1993-10-11, by wenzelm
removed ndependent_tr (no longer needed, use _K);
1993-10-11, by wenzelm
*** empty log message ***
1993-10-11, by wenzelm
*** empty log message ***
1993-10-08, by wenzelm
fixed comment;
1993-10-08, by wenzelm
added parse rule for "<*>";
1993-10-08, by wenzelm
@List: replaced "args" by "is";
1993-10-08, by wenzelm
*** empty log message ***
1993-10-08, by wenzelm
added cons, rcons, last_elem, sort_strings, take_suffix;
1993-10-08, by wenzelm
added raise_type: string -> typ list -> term list -> 'a;
1993-10-08, by wenzelm
"The error/exception above ...": errorneous goal now quoted;
1993-10-08, by wenzelm
used ~: for "not in"
1993-10-07, by lcp
added ~: for "not in"
1993-10-07, by lcp
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