5 *** Overview of INCOMPATIBILITIES *** 
5 *** Overview of INCOMPATIBILITIES *** 
6 
6 
7 * HOL: induct renamed to lfp_induct; 
7 * HOL: induct renamed to lfp_induct; 
8 
8 
9 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; 
9 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; 

10 

11 * Isar: 'obtain' no longer declares "that" fact as simp/intro; 
10 
12 
11 
13 
12 *** Document preparation *** 
14 *** Document preparation *** 
13 
15 
14 * improved isabelle style files; more abstract symbol implementation 
16 * improved isabelle style files; more abstract symbol implementation 
22 that presentation of goal states does not conform to actual 
24 that presentation of goal states does not conform to actual 
23 humanreadable proof documents. Please do not include goal states 
25 humanreadable proof documents. Please do not include goal states 
24 into document output unless you really know what you are doing! 
26 into document output unless you really know what you are doing! 
25 
27 
26 
28 
27 

28 *** Isar *** 
29 *** Isar *** 
29 
30 
30 * HOL: default proof step now includes 'intro_classes'; 
31 * Pure: assumption method (an implicit finishing) now handles actual 

32 rules as well; 

33 

34 * Pure: improved 'obtain'  moved to Pure, insert "that" into 

35 initial goal, declare "that" only as Pure intro (only for single 

36 steps); the "that" rule assumption may now be involved in implicit 

37 finishing, thus ".." becomes a feasible for trivial obtains; 

38 

39 * Pure: default proof step now includes 'intro_classes'; thus trivial 

40 instance proofs may be performed by ".."; 

41 

42 * Pure: ?thesis / ?this / "..." now work for pure metalevel 

43 statements as well; 
31 
44 
32 
45 
33 *** HOL *** 
46 *** HOL *** 
34 
47 
35 * HOL/Library: a collection of generic theories to be used together 
48 * HOL/Library: a collection of generic theories to be used together 
36 with main HOL; the theory loader path already includes this directory 
49 with main HOL; the theory loader path already includes this directory 
37 by default; the following existing theories have been moved here: 
50 by default; the following existing theories have been moved here: 
38 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While 
51 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While 
39 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); 
52 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); 

53 

54 * HOL/typedef: simplified package, provide more useful rules (see also 

55 HOL/subset.thy); 

56 

57 

58 *** General *** 

59 

60 * Provers: fast_tac (and friends) now handle actual objectlogic rules 

61 as assumptions as well; 

62 
40 
63 
41 
64 
42 New in Isabelle991 (October 2000) 
65 New in Isabelle991 (October 2000) 
43  
66  
44 
67 