1997-02-28 paulson 1997-02-28 rule_by_tactic no longer standardizes its result
1997-02-28 paulson 1997-02-28 Addition of de Bruijn formulae
1997-02-27 wenzelm 1997-02-27 tuned comment;
1997-02-27 wenzelm 1997-02-27 tuned comments;
1997-02-25 wenzelm 1997-02-25 added proper subset symbols syntax;
1997-02-25 pusch 1997-02-25 minor changes due to primrec defintions for +,-,*
1997-02-25 pusch 1997-02-25 minor changes due to new primrec definitions for +,-,*
1997-02-25 pusch 1997-02-25 definitions of +,-,* replaced by primrec definitions
1997-02-25 pusch 1997-02-25 function nat_add_primrec added to allow primrec definitions over nat
1997-02-24 oheimb 1997-02-24 removed explicit_domains/, which is now covered by ex/
1997-02-24 wenzelm 1997-02-24 added "_" syntax for dummyT;
1997-02-21 wenzelm 1997-02-21 declared the dummy type;
1997-02-21 wenzelm 1997-02-21 replaced natural by subset;
1997-02-21 wenzelm 1997-02-21 tuned symbolic [|_|] syntax;
1997-02-21 wenzelm 1997-02-21 tuned some chars;
1997-02-21 paulson 1997-02-21 More robust proof (?)
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1997-02-21 paulson 1997-02-21 Introduction of rotate_rule
1997-02-21 wenzelm 1997-02-21 removed empty line (which broke xfedor);
1997-02-21 wenzelm 1997-02-21 don't hack, use xfed or xfedor;
1997-02-21 wenzelm 1997-02-21 fixed Id comment;
1997-02-20 wenzelm 1997-02-20 makedist -- make Isabelle distribution.
1997-02-20 wenzelm 1997-02-20 tuned URL;
1997-02-20 wenzelm 1997-02-20 added index info;
1997-02-20 wenzelm 1997-02-20 index info;
1997-02-20 wenzelm 1997-02-20 added dist;
1997-02-20 wenzelm 1997-02-20 some administrative tools for the Isabelle;
1997-02-20 wenzelm 1997-02-20 made a bit more robust for 'make dist';
1997-02-20 wenzelm 1997-02-20 rail output;
1997-02-20 wenzelm 1997-02-20 fixed rail.sty dep;
1997-02-20 wenzelm 1997-02-20 added this file;
1997-02-20 wenzelm 1997-02-20 rail output;
1997-02-20 wenzelm 1997-02-20 made a bit more robust;
1997-02-17 wenzelm 1997-02-17 manual steps comment;
1997-02-17 wenzelm 1997-02-17 *** empty log message ***
1997-02-17 slotosch 1997-02-17 described changes for HOLCF-Version without rules and arities
1997-02-17 wenzelm 1997-02-17 file moved;
1997-02-17 wenzelm 1997-02-17 file moved here;
1997-02-17 wenzelm 1997-02-17 configure - adapt Isabelle distribution to system environment
1997-02-17 oheimb 1997-02-17 improved description of recent changes
1997-02-17 slotosch 1997-02-17 reflecting recent changes of the simplifier
1997-02-17 oheimb 1997-02-17 corrected type of plift
1997-02-17 oheimb 1997-02-17 reflecting recent changes of the simplifier
1997-02-17 wenzelm 1997-02-17 mk_rews: automatically includes strip_shyps, zero_var_indexes;
1997-02-17 slotosch 1997-02-17 New file for theorems of Porder0 Dervie the prperties of partial orders from the axiomatic type class po
1997-02-17 wenzelm 1997-02-17 tuned comments;
1997-02-17 slotosch 1997-02-17 Examples are adopted to the changes from HOLCF. Classlib is reduced. Classlib still uses arities, Classlib will change completely to new classes of ADTs
1997-02-17 slotosch 1997-02-17 using types one = unit lift and translations causes troubles between the type one and the constant one. The later was changed to ONE
1997-02-17 slotosch 1997-02-17 Changes of HOLCF from Oscar Slotosch: 1. axclass instead of class * less instead of less_fun, less_cfun, less_sprod, less_cprod, less_ssum, less_up, less_lift * @x.!y.x<<y instead of UUU instead of UU_fun, UU_cfun, ... * no witness type void needed (eliminated Void.thy.Void.ML) * inst_<typ>_<class> derived as theorems 2. improved some proves on less_sprod and less_cprod * eliminated the following theorems Sprod1.ML: less_sprod1a Sprod1.ML: less_sprod1b Sprod1.ML: less_sprod2a Sprod1.ML: less_sprod2b Sprod1.ML: less_sprod2c Sprod2.ML: less_sprod3a Sprod2.ML: less_sprod3b Sprod2.ML: less_sprod4b Sprod2.ML: less_sprod4c Sprod3.ML: less_sprod5b Sprod3.ML: less_sprod5c Cprod1.ML: less_cprod1b Cprod1.ML: less_cprod2a Cprod1.ML: less_cprod2b Cprod1.ML: less_cprod2c Cprod2.ML: less_cprod3a Cprod2.ML: less_cprod3b 3. new classes: * cpo<po, * chfin<pcpo, * flat<pcpo, * derived: flat<chfin to do: show instances for lift 4. Data Type One * Used lift for the definition: one = unit lift * Changed the constant one into ONE 5. Data Type Tr * Used lift for the definition: tr = bool lift * adopted definitions of if,andalso,orelse,neg * only one theory Tr.thy,Tr.ML instead of Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML * reintroduced ceils for =TT,=FF 6. typedef * Using typedef instead of faking type definitions to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun 7. adopted examples and domain construct to theses changes These changes eliminated all rules and arities from HOLCF
1997-02-15 oheimb 1997-02-15 *** empty log message ***
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the classical reasoner
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1997-02-15 oheimb 1997-02-15 added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss, safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions new addss (old version retained as unsafe_addss), new Addss (old version retained as Unsafe_Addss), new auto_tac (old version retained as unsafe_auto_tac),
1997-02-15 oheimb 1997-02-15 cosmetic
1997-02-15 oheimb 1997-02-15 updated mini_ss
1997-02-15 oheimb 1997-02-15 added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss, safe_asm_more_full_simp_tac new addss (old version retained as unsafe_addss), new auto_tac (old version retained as unsafe_auto_tac), clasimpset with modification functions
1997-02-15 oheimb 1997-02-15 corrected minor mistakes
1997-02-15 oheimb 1997-02-15 description of safe vs. unsafe wrapper and the functions involved
1997-02-15 oheimb 1997-02-15 moved THEN_MAYBE to Pure/tctical.ML better addbefore, addafter (now: addaltern), setwrapper (now: setWrapper) and addwrapper (now addWrapper) added safe wrapper(and functions setSWrapper,compSWrapper,addSbefore,addSaltern)
1997-02-15 oheimb 1997-02-15 added deleqcongs, richer rep_ss split solver in safe and unsafe parts (finish_tac, unsafe_finish_tac) added safe_asm_full_simp_tac, setSSolver, addSSolver renamed setsolver to setSolver, addsolver to addSolver