7 *** General *** 
7 *** General *** 
8 
8 
9 * Command 'find_theorems': support "*" wildcard in "name:" criterion. 
9 * Command 'find_theorems': support "*" wildcard in "name:" criterion. 
10 
10 
11 
11 

12 *** Document preparation *** 

13 

14 * Added antiquotations @{ML_type text} and @{ML_struct} which check 

15 the given source text as ML type/structure, printing verbatim. 

16 

17 
12 *** Pure *** 
18 *** Pure *** 

19 

20 * Isar: improper proof element 'guess' is like 'obtain', but derives 

21 the obtained context from the course of reasoning! For example: 

22 

23 assume "EX x y. A x & B y"  "any previous fact" 

24 then guess x and y by clarify 

25 

26 This technique is potentially adventurous, depending on the facts and 

27 proof tools being involved here. 
13 
28 
14 * Input syntax now supports dummy variable binding "%_. b", where the 
29 * Input syntax now supports dummy variable binding "%_. b", where the 
15 body does not mention the bound variable. Note that dummy patterns 
30 body does not mention the bound variable. Note that dummy patterns 
16 implicitly depend on their context of bounds, which makes "{_. _}" 
31 implicitly depend on their context of bounds, which makes "{_. _}" 
17 match any set comprehension as expected. Potential INCOMPATIBILITY  
32 match any set comprehension as expected. Potential INCOMPATIBILITY  
20 
35 
21 * Removed obsolete syntactic constant "_K" and its associated parse 
36 * Removed obsolete syntactic constant "_K" and its associated parse 
22 translation. INCOMPATIBILITY  use dummy abstraction instead, for 
37 translation. INCOMPATIBILITY  use dummy abstraction instead, for 
23 example "A > B" => "Pi A (%_. B)". 
38 example "A > B" => "Pi A (%_. B)". 
24 
39 

40 
25 *** HOL *** 
41 *** HOL *** 
26 
42 
27 * In the context of the assumption "~(s = t)" the simplifier rewrites 
43 * In the context of the assumption "~(s = t)" the Simplifier rewrites 
28 "t = s" to False (by simproc "neq_simproc"). For backward compatibility 
44 "t = s" to False (by simproc "neq_simproc"). For backward 
29 this can be disabled by ML"reset use_neq_simproc". 
45 compatibility this can be disabled by ML "reset use_neq_simproc". 
30 
46 
31 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals 
47 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals 
32 no longer need to be stated as "<prems> ==> False", equivalences (i.e. 
48 no longer need to be stated as "<prems> ==> False", equivalences (i.e. 
33 "=" on type bool) are handled, variable names of the form "lit_<n>" are 
49 "=" on type bool) are handled, variable names of the form "lit_<n>" 
34 no longer reserved, significant speedup. 
50 are no longer reserved, significant speedup. 

51 
35 
52 
36 
53 
37 New in Isabelle2005 (October 2005) 
54 New in Isabelle2005 (October 2005) 
38  
55  
39 
56 