3 ================================================ 
3 ================================================ 
4 
4 
5 New in Isabelle948 (April 1997) 
5 New in Isabelle948 (April 1997) 
6  
6  
7 
7 
8 * reimplemented type inference; 
8 *** General Changes *** 

9 

10 * new utilities to build / run / maintain Isabelle etc. (in parts 

11 still somewhat experimental); old Makefiles etc. still functional; 
9 
12 
10 * INSTALL text, together with ./configure and ./build scripts; 
13 * INSTALL text, together with ./configure and ./build scripts; 

14 

15 * reimplemented type inference for greater efficiency; 

16 

17 * prlim command for dealing with lots of subgoals (an easier way of 

18 setting goals_limit); 

19 

20 *** Syntax 

21 

22 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to 

23 be used in conjunction with the Isabelle symbol font; uses the 

24 "symbols" syntax table; 
11 
25 
12 * added token_translation interface (may translate name tokens in 
26 * added token_translation interface (may translate name tokens in 
13 arbitrary ways, dependent on their type (free, bound, tfree, ...) and 
27 arbitrary ways, dependent on their type (free, bound, tfree, ...) and 
14 the current print_mode); 
28 the current print_mode); 
15 
29 
16 * token translations for modes "xterm" and "xterm_color" that display 
30 * token translations for modes "xterm" and "xterm_color" that display 
17 names in bold, underline etc. or colors; 
31 names in bold, underline etc. or colors; 

32 

33 * now supports alternative (named) syntax tables (parser and pretty 

34 printer); internal interface is provided by add_modesyntax(_i); 

35 

36 * infixes may now be declared with names independent of their syntax; 

37 

38 * added typed_print_translation (like print_translation, but may 

39 access type of constant); 

40 

41 *** Classical Reasoner *** 

42 

43 Blast_tac: a new tactic! It is often more powerful than fast_tac, but has 

44 some limitations. Blast_tac... 

45 + ignores addss, addbefore, addafter; this restriction is intrinsic 

46 + ignores elimination rules that don't have the correct format 

47 (the conclusion MUST be a formula variable) 

48 + ignores types, which can make HOL proofs fail 

49 + rules must not require higherorder unification, e.g. apply_type in ZF 

50 [message "Function Var's argument not a bound variable" relates to this] 

51 + its proof strategy is more general but can actually be slower 

52 

53 * substitution with equality assumptions no longer permutes other assumptions. 

54 

55 * minor changes in semantics of addafter (now called addaltern); renamed 

56 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper 

57 (and access functions for it) 

58 

59 * improved combination of classical reasoner and simplifier: new 

60 addss, auto_tac, functions for handling clasimpsets, ... Now, the 

61 simplification is safe (therefore moved to safe_step_tac) and thus 

62 more complete, as multiple instantiation of unknowns (with slow_tac). 

63 COULD MAKE EXISTING PROOFS FAIL; in case of problems with 

64 old proofs, use unsafe_addss and unsafe_auto_tac 

65 

66 *** Simplifier *** 

67 

68 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. 

69 

70 * the solver is now split into a safe and an unsafe part. 

71 This should be invisible for the normal user, except that the 

72 functions setsolver and addsolver have been renamed to setSolver and 

73 addSolver. added safe_asm_full_simp_tac. 

74 

75 * ordering on terms as parameter (used for ordered rewriting); 

76 added interface for simplification procedures (functions that produce *proven* 

77 rewrite rules on the fly, depending on current redex); 

78 

79 *** HOL *** 

80 

81 * patterns in case expressions allow tuple patterns as arguments to 

82 constructors, for example `case x of [] => ...  (x,y,z)#ps => ...' 

83 

84 * primrec now also works with type nat; 

85 

86 * the constant for negation has been renamed from "not" to "Not" to 

87 harmonize with FOL, ZF, LK, etc. 

88 

89 * HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists 

90 

91 * HOL/ex/Ring.thy declares cring_simp, which solves equational 

92 problems in commutative rings, using axiomatic type classes for + and *; 

93 

94 * more examples in HOL/MiniML and HOL/Auth; 

95 

96 * more default rewrite rules for quantifiers, union/intersection; 
18 
97 
19 * HOLCF changes: derived all rules and arities 
98 * HOLCF changes: derived all rules and arities 
20 + axiomatic type classes instead of classes 
99 + axiomatic type classes instead of classes 
21 + typedef instead of faking type definitions 
100 + typedef instead of faking type definitions 
22 + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc. 
101 + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc. 
24 + eliminated the types void, one, tr 
103 + eliminated the types void, one, tr 
25 + use unit lift and bool lift (with translations) instead of one and tr 
104 + use unit lift and bool lift (with translations) instead of one and tr 
26 + eliminated blift from Lift3.thy (use Def instead of blift) 
105 + eliminated blift from Lift3.thy (use Def instead of blift) 
27 all eliminated rules are derived as theorems > no visible changes 
106 all eliminated rules are derived as theorems > no visible changes 
28 
107 
29 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. 
108 *** ZF *** 
30 

31 * simplifier: the solver is now split into a safe and an unsafe part. 

32 This should be invisible for the normal user, except that the 

33 functions setsolver and addsolver have been renamed to setSolver and 

34 addSolver. added safe_asm_full_simp_tac. 

35 

36 * classical reasoner: substitution with equality assumptions no longer 

37 permutes other assumptions. 

38 

39 * classical reasoner: minor changes in semantics of addafter (now called 

40 addaltern); renamed setwrapper to setWrapper and compwrapper to compWrapper; 

41 added safe wrapper (and access functions for it) 

42 

43 * improved combination of classical reasoner and simplifier: new 

44 addss, auto_tac, functions for handling clasimpsets, ... Now, the 

45 simplification is safe (therefore moved to safe_step_tac) and thus 

46 more complete, as multiple instantiation of unknowns (with slow_tac). 

47 COULD MAKE EXISTING PROOFS FAIL; in case of problems with 

48 old proofs, use unsafe_addss and unsafe_auto_tac 

49 

50 * HOL: patterns in case expressions allow tuple patterns as arguments to 

51 constructors, for example `case x of [] => ...  (x,y,z)#ps => ...' 

52 

53 * HOL: primrec now also works with type nat; 

54 

55 * HOL: the constant for negation has been renamed from "not" to "Not" to 

56 harmonize with FOL, ZF, LK, etc. 

57 

58 * new utilities to build / run / maintain Isabelle etc. (in parts 

59 still somewhat experimental); old Makefiles etc. still functional; 

60 

61 * simplifier: termless order as parameter; added interface for 

62 simplification procedures (functions that produce *proven* rewrite 

63 rules on the fly, depending on current redex); 

64 

65 * now supports alternative (named) syntax tables (parser and pretty 

66 printer); internal interface is provided by add_modesyntax(_i); 

67 

68 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to 

69 be used in conjunction with the Isabelle symbol font; uses the 

70 "symbols" syntax table; 

71 

72 * infixes may now be declared with names independent of their syntax; 

73 

74 * added typed_print_translation (like print_translation, but may 

75 access type of constant); 

76 

77 * prlim command for dealing with lots of subgoals (an easier way of 

78 setting goals_limit); 

79 

80 * HOL/ex/Ring.thy declares cring_simp, which solves equational 

81 problems in commutative rings, using axiomatic type classes for + and *; 

82 
109 
83 * ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default 
110 * ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default 
84 rewrite rule; this may affect some proofs. eq_cs is gone but can be put back 
111 rewrite rule; this may affect some proofs. eq_cs is gone but can be put back 
85 as ZF_cs addSIs [equalityI]; 
112 as ZF_cs addSIs [equalityI]; 
86 

87 * more examples in HOL/MiniML and HOL/Auth; 

88 

89 * more default rewrite rules in HOL for quantifiers, union/intersection; 

90 

91 * the NEWS file; 

92 
113 
93 
114 
94 
115 
95 New in Isabelle947 (November 96) 
116 New in Isabelle947 (November 96) 
96  
117  