Mon, 17 Feb 1997 16:50:59 +0100 improved description of recent changes
oheimb [Mon, 17 Feb 1997 16:50:59 +0100] rev 2649
improved description of recent changes
Mon, 17 Feb 1997 16:50:17 +0100 reflecting recent changes of the simplifier
slotosch [Mon, 17 Feb 1997 16:50:17 +0100] rev 2648
reflecting recent changes of the simplifier
Mon, 17 Feb 1997 16:31:37 +0100 corrected type of plift
oheimb [Mon, 17 Feb 1997 16:31:37 +0100] rev 2647
corrected type of plift
Mon, 17 Feb 1997 16:01:16 +0100 reflecting recent changes of the simplifier
oheimb [Mon, 17 Feb 1997 16:01:16 +0100] rev 2646
reflecting recent changes of the simplifier
Mon, 17 Feb 1997 13:54:24 +0100 mk_rews: automatically includes strip_shyps, zero_var_indexes;
wenzelm [Mon, 17 Feb 1997 13:54:24 +0100] rev 2645
mk_rews: automatically includes strip_shyps, zero_var_indexes;
Mon, 17 Feb 1997 13:26:32 +0100 New file for theorems of Porder0
slotosch [Mon, 17 Feb 1997 13:26:32 +0100] rev 2644
New file for theorems of Porder0 Dervie the prperties of partial orders from the axiomatic type class po
Mon, 17 Feb 1997 12:00:00 +0100 tuned comments;
wenzelm [Mon, 17 Feb 1997 12:00:00 +0100] rev 2643
tuned comments;
Mon, 17 Feb 1997 11:04:00 +0100 Examples are adopted to the changes from HOLCF.
slotosch [Mon, 17 Feb 1997 11:04:00 +0100] rev 2642
Examples are adopted to the changes from HOLCF. Classlib is reduced. Classlib still uses arities, Classlib will change completely to new classes of ADTs
Mon, 17 Feb 1997 11:01:10 +0100 using types one = unit lift and translations causes troubles between
slotosch [Mon, 17 Feb 1997 11:01:10 +0100] rev 2641
using types one = unit lift and translations causes troubles between the type one and the constant one. The later was changed to ONE
Mon, 17 Feb 1997 10:57:11 +0100 Changes of HOLCF from Oscar Slotosch:
slotosch [Mon, 17 Feb 1997 10:57:11 +0100] rev 2640
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
Sat, 15 Feb 1997 18:24:05 +0100 *** empty log message ***
oheimb [Sat, 15 Feb 1997 18:24:05 +0100] rev 2639
*** empty log message ***
Sat, 15 Feb 1997 17:55:11 +0100 reflecting my recent changes of the classical reasoner
oheimb [Sat, 15 Feb 1997 17:55:11 +0100] rev 2638
reflecting my recent changes of the classical reasoner
Sat, 15 Feb 1997 17:52:31 +0100 reflecting my recent changes of the simplifier and classical reasoner
oheimb [Sat, 15 Feb 1997 17:52:31 +0100] rev 2637
reflecting my recent changes of the simplifier and classical reasoner
Sat, 15 Feb 1997 17:48:19 +0100 added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb [Sat, 15 Feb 1997 17:48:19 +0100] rev 2636
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),
Sat, 15 Feb 1997 17:45:08 +0100 cosmetic
oheimb [Sat, 15 Feb 1997 17:45:08 +0100] rev 2635
cosmetic
Sat, 15 Feb 1997 17:44:10 +0100 updated mini_ss
oheimb [Sat, 15 Feb 1997 17:44:10 +0100] rev 2634
updated mini_ss
Sat, 15 Feb 1997 17:43:27 +0100 added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb [Sat, 15 Feb 1997 17:43:27 +0100] rev 2633
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
Sat, 15 Feb 1997 17:35:53 +0100 corrected minor mistakes
oheimb [Sat, 15 Feb 1997 17:35:53 +0100] rev 2632
corrected minor mistakes
Sat, 15 Feb 1997 17:02:19 +0100 description of safe vs. unsafe wrapper and the functions involved
oheimb [Sat, 15 Feb 1997 17:02:19 +0100] rev 2631
description of safe vs. unsafe wrapper and the functions involved
Sat, 15 Feb 1997 16:23:58 +0100 moved THEN_MAYBE to Pure/tctical.ML
oheimb [Sat, 15 Feb 1997 16:23:58 +0100] rev 2630
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)
Sat, 15 Feb 1997 16:14:35 +0100 added deleqcongs, richer rep_ss
oheimb [Sat, 15 Feb 1997 16:14:35 +0100] rev 2629
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
Sat, 15 Feb 1997 16:10:00 +0100 description of del(eq)congs, safe and unsafe solver
oheimb [Sat, 15 Feb 1997 16:10:00 +0100] rev 2628
description of del(eq)congs, safe and unsafe solver
Sat, 15 Feb 1997 16:05:07 +0100 added THEN_MAYBE and THEN_MAYBE'
oheimb [Sat, 15 Feb 1997 16:05:07 +0100] rev 2627
added THEN_MAYBE and THEN_MAYBE'
Sat, 15 Feb 1997 16:04:33 +0100 added del_congs
oheimb [Sat, 15 Feb 1997 16:04:33 +0100] rev 2626
added del_congs
Fri, 14 Feb 1997 16:01:43 +0100 Some lemmas changed to valuesd
narasche [Fri, 14 Feb 1997 16:01:43 +0100] rev 2625
Some lemmas changed to valuesd
Fri, 14 Feb 1997 15:32:00 +0100 fixed comment;
wenzelm [Fri, 14 Feb 1997 15:32:00 +0100] rev 2624
fixed comment;
Fri, 14 Feb 1997 15:29:20 +0100 improved interface options;
wenzelm [Fri, 14 Feb 1997 15:29:20 +0100] rev 2623
improved interface options;
Fri, 14 Feb 1997 15:16:21 +0100 semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm [Fri, 14 Feb 1997 15:16:21 +0100] rev 2622
semi fix of piping-quit peoblem (should work on systems with *real* sh);
Fri, 14 Feb 1997 15:13:32 +0100 globally unset ENV, BASH_ENV;
wenzelm [Fri, 14 Feb 1997 15:13:32 +0100] rev 2621
globally unset ENV, BASH_ENV;
Fri, 14 Feb 1997 12:19:42 +0100 Made troublesome simplifier warning dependent on trace_simp.
nipkow [Fri, 14 Feb 1997 12:19:42 +0100] rev 2620
Made troublesome simplifier warning dependent on trace_simp.
Fri, 14 Feb 1997 11:40:53 +0100 Modified and shortened adm_disj lemmas.
nipkow [Fri, 14 Feb 1997 11:40:53 +0100] rev 2619
Modified and shortened adm_disj lemmas.
Fri, 14 Feb 1997 10:57:17 +0100 Deleted a useless definition
paulson [Fri, 14 Feb 1997 10:57:17 +0100] rev 2618
Deleted a useless definition
Fri, 14 Feb 1997 10:41:02 +0100 Added optimization: do nothing for empty list
paulson [Fri, 14 Feb 1997 10:41:02 +0100] rev 2617
Added optimization: do nothing for empty list
Fri, 14 Feb 1997 10:40:23 +0100 A bit more pattern-matching in eta_contract
paulson [Fri, 14 Feb 1997 10:40:23 +0100] rev 2616
A bit more pattern-matching in eta_contract
Fri, 14 Feb 1997 10:38:48 +0100 Tidying and a corrected comment
paulson [Fri, 14 Feb 1997 10:38:48 +0100] rev 2615
Tidying and a corrected comment
Fri, 14 Feb 1997 10:36:33 +0100 Added a new challenge problem
paulson [Fri, 14 Feb 1997 10:36:33 +0100] rev 2614
Added a new challenge problem
Fri, 14 Feb 1997 10:35:42 +0100 Updated documentation of IFOL_ss
paulson [Fri, 14 Feb 1997 10:35:42 +0100] rev 2613
Updated documentation of IFOL_ss
Fri, 14 Feb 1997 10:35:23 +0100 Documented thin_tac
paulson [Fri, 14 Feb 1997 10:35:23 +0100] rev 2612
Documented thin_tac
Fri, 14 Feb 1997 10:35:06 +0100 Strengthened warnings concerning topthm(), etc.
paulson [Fri, 14 Feb 1997 10:35:06 +0100] rev 2611
Strengthened warnings concerning topthm(), etc.
Fri, 14 Feb 1997 10:34:24 +0100 Updated a reference
paulson [Fri, 14 Feb 1997 10:34:24 +0100] rev 2610
Updated a reference
Wed, 12 Feb 1997 18:54:39 +0100 New class "order" and accompanying changes.
nipkow [Wed, 12 Feb 1997 18:54:39 +0100] rev 2609
New class "order" and accompanying changes.
Wed, 12 Feb 1997 18:53:59 +0100 New class "order" and accompanying changes.
nipkow [Wed, 12 Feb 1997 18:53:59 +0100] rev 2608
New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
Wed, 12 Feb 1997 15:43:50 +0100 TFL: missing -q option!
wenzelm [Wed, 12 Feb 1997 15:43:50 +0100] rev 2607
TFL: missing -q option!
Wed, 12 Feb 1997 15:42:31 +0100 tuned names: partial order, linear order;
wenzelm [Wed, 12 Feb 1997 15:42:31 +0100] rev 2606
tuned names: partial order, linear order;
Mon, 10 Feb 1997 16:16:55 +0100 tuned startup;
wenzelm [Mon, 10 Feb 1997 16:16:55 +0100] rev 2605
tuned startup; semi fix of piping-quit peoblem (should work on systems with *real& sh);
Mon, 10 Feb 1997 15:45:31 +0100 fixed comment;
wenzelm [Mon, 10 Feb 1997 15:45:31 +0100] rev 2604
fixed comment;
Mon, 10 Feb 1997 12:52:11 +0100 Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson [Mon, 10 Feb 1997 12:52:11 +0100] rev 2603
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
Mon, 10 Feb 1997 12:34:54 +0100 Renamed structure Int (intuitionistic prover) to IntPr
paulson [Mon, 10 Feb 1997 12:34:54 +0100] rev 2602
Renamed structure Int (intuitionistic prover) to IntPr
Mon, 10 Feb 1997 12:31:54 +0100 Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson [Mon, 10 Feb 1997 12:31:54 +0100] rev 2601
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
Fri, 07 Feb 1997 17:15:30 +0100 removed ISABELLE_INTERFACE_OPTIONS;
wenzelm [Fri, 07 Feb 1997 17:15:30 +0100] rev 2600
removed ISABELLE_INTERFACE_OPTIONS;
Fri, 07 Feb 1997 17:14:56 +0100 tuned;
wenzelm [Fri, 07 Feb 1997 17:14:56 +0100] rev 2599
tuned; removed ISABELLE_INTERFACE_OPTIONS;
Fri, 07 Feb 1997 17:14:33 +0100 tuned;
wenzelm [Fri, 07 Feb 1997 17:14:33 +0100] rev 2598
tuned; removed ISABELLE_SYMBOLS;
Fri, 07 Feb 1997 14:15:35 +0100 Modified proofs due to added triv_forall_equality.
nipkow [Fri, 07 Feb 1997 14:15:35 +0100] rev 2597
Modified proofs due to added triv_forall_equality.
Fri, 07 Feb 1997 14:13:58 +0100 Modified proofs because of added "triv_forall_equality".
nipkow [Fri, 07 Feb 1997 14:13:58 +0100] rev 2596
Modified proofs because of added "triv_forall_equality".
Fri, 07 Feb 1997 14:13:20 +0100 Added "triv_forall_equality" to HOL_ss.
nipkow [Fri, 07 Feb 1997 14:13:20 +0100] rev 2595
Added "triv_forall_equality" to HOL_ss.
Thu, 06 Feb 1997 18:40:39 +0100 functionality added to getsettings;
wenzelm [Thu, 06 Feb 1997 18:40:39 +0100] rev 2594
functionality added to getsettings;
Thu, 06 Feb 1997 18:40:23 +0100 removed getplatform, ISABELLE_OUTPUT_DIR;
wenzelm [Thu, 06 Feb 1997 18:40:23 +0100] rev 2593
removed getplatform, ISABELLE_OUTPUT_DIR;
Thu, 06 Feb 1997 18:33:50 +0100 removed getplatform, ISABELLE_OUTPUT_DIR;
wenzelm [Thu, 06 Feb 1997 18:33:50 +0100] rev 2592
removed getplatform, ISABELLE_OUTPUT_DIR;
Thu, 06 Feb 1997 18:31:27 +0100 removed getplatform;
wenzelm [Thu, 06 Feb 1997 18:31:27 +0100] rev 2591
removed getplatform;
Thu, 06 Feb 1997 18:27:47 +0100 integrated getplatform stuff;
wenzelm [Thu, 06 Feb 1997 18:27:47 +0100] rev 2590
integrated getplatform stuff; added ISABELLE_OUTPUT_DIR;
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip