Old_HOL: Graph

Mercurial Mercurial > repos > Old_HOL / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -100 -60 tip

update tags default tip
2009-07-23, by convert-repo
removed them again
1996-01-19, by clasohm
accidentally deleted these files from the repository; now adding them and
1996-01-19, by clasohm
Old_HOL removed from the distribution
1996-01-19, by clasohm
added calls of init_html and make_chart Isabelle94-5
1995-10-24, by clasohm
changed HOL to Old_HOL Isabelle94-4
1995-06-29, by clasohm
removed \...\ inside strings
1995-06-21, by clasohm
Simplified some proofs and made them work for new hyp_subst_tac. Isabelle94-3
1995-04-14, by lcp
Removed the "exit 1" calls, since now the
1995-04-06, by lcp
Deleted extra space in clos_mk.
1995-04-06, by lcp
Simplified some proofs and made them work for new hyp_subst_tac.
1995-04-06, by lcp
Ran expandshort
1995-04-06, by lcp
Removed the "exit 1" calls, since now the
1995-04-06, by lcp
Deleted some useless things and made proofs of
1995-04-06, by lcp
Removed the "exit 1" calls, since now the
1995-04-06, by lcp
Set up for new hyp_subst_tac.
1995-04-06, by lcp
Changed proof of lessE for new hyp_subst_tac
1995-04-06, by lcp
Added Id: line
1995-04-06, by lcp
replaced 'arities' by 'instance';
1995-03-31, by wenzelm
Defined addss to perform simplification in a claset.
1995-03-30, by lcp
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
1995-03-28, by clasohm
Added recursion equations for foldl to list_ss.
1995-03-27, by nipkow
Added a few thms to nat_ss and list_ss
1995-03-17, by nipkow
Now calls exit_use instead of use, for prompt failure if errors are detected.
1995-03-15, by lcp
Removed some type constraints
1995-03-14, by nipkow
added "exit 1"
1995-03-14, by nipkow
Removed unecessary type constraint because instantiations do not freeze type
1995-03-13, by nipkow
Added dependencies on ../Provers/hypsubst.ML and removed those on
1995-03-08, by nipkow
Enforced partial evaluation of mk_case_split_tac
1995-03-08, by nipkow
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
1995-03-01, by lcp
Proofs of inv1 and inv4 now use less_le_trans instead of
1995-03-01, by lcp
Renamed plus_leD1 to add_leD1.
1995-03-01, by lcp
Proved inj_onto_iff
1995-03-01, by lcp
No longer calls maketest; instead, the Makefile writes the file
1995-02-28, by lcp
Re-organised to perform the tests independently. Now test
1995-02-28, by lcp
Installation of Integ (ported from ZF by Mattolini)
1995-02-28, by lcp
Proved less_eq_Suc_add and add_left_cancel (cf left_plus_cancel on
1995-02-28, by lcp
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
1995-02-27, by lcp
Installation of Integ (ported from ZF by Mattolini)
1995-02-27, by lcp
Installation of Integ (ported from ZF by Mattolini)
1995-02-27, by lcp
Reorganized/optimized datatype definitions.
1995-02-19, by nipkow
pair_ss -> prod_ss.
1995-02-16, by nipkow
Removed pair_ss because identical to prod_ss.
1995-02-16, by nipkow
Added "flat"
1995-02-13, by nipkow
Norbert's update allowing nested calls in primrec.
1995-02-08, by nipkow
More rewrite rules.
1995-02-08, by nipkow
Add dependence on ex/String.thy/ML
1995-02-03, by nipkow
Added Markus Wenzel's string representation.
1995-02-03, by nipkow
Simplified proof.
1995-02-01, by nipkow
The thm if(P,Q,R) now yields the two conditional rewrite rules P ==> Q and
1995-02-01, by nipkow
Added Un_empty (also to set_ss)
1995-01-30, by nipkow
Added some simplifications for ? x.
1995-01-29, by nipkow
Added "nth" and some lemmas.
1995-01-26, by nipkow
added bind_thm for theorems made by "standard ..." Isabelle94-2
1994-12-14, by clasohm
improved primrec: now calls store_thm;
1994-12-14, by wenzelm
removed HOL_Lemmas structure and added qed_goal
1994-12-09, by clasohm
replaced store_thm by bind_thm
1994-12-08, by clasohm
Added (? x. x=t & P) = P to the simpset.
1994-12-07, by nipkow
Removed a local lemma which is now part of HOL_ss.
1994-12-07, by nipkow
Moved the old List to ex and replaced it by one defined via
1994-12-02, by nipkow

less more | (0) -100 -60 tip

Old_HOL