43 context discipline. See also Assumption.add_assumes and the more |
43 context discipline. See also Assumption.add_assumes and the more |
44 primitive Thm.assume_hyps. |
44 primitive Thm.assume_hyps. |
45 |
45 |
46 |
46 |
47 *** HOL *** |
47 *** HOL *** |
|
48 |
|
49 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL". |
|
50 The "bnf", "wrap_free_constructors", "datatype_new", "codatatype", |
|
51 "primrec_new", "primcorec", and "primcorecursive" command are now part of |
|
52 "Main". |
|
53 INCOMPATIBILITY. |
|
54 Theory renamings: |
|
55 FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) |
|
56 Library/Wfrec.thy ~> Wfrec.thy |
|
57 Library/Zorn.thy ~> Zorn.thy |
|
58 Cardinals/Order_Relation.thy ~> Order_Relation.thy |
|
59 Library/Order_Union.thy ~> Cardinals/Order_Union.thy |
|
60 Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy |
|
61 Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy |
|
62 Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy |
|
63 Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy |
|
64 Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy |
|
65 BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy |
|
66 BNF/Basic_BNFs.thy ~> Basic_BNFs.thy |
|
67 BNF/BNF_Comp.thy ~> BNF_Comp.thy |
|
68 BNF/BNF_Def.thy ~> BNF_Def.thy |
|
69 BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy |
|
70 BNF/BNF_GFP.thy ~> BNF_GFP.thy |
|
71 BNF/BNF_LFP.thy ~> BNF_LFP.thy |
|
72 BNF/BNF_Util.thy ~> BNF_Util.thy |
|
73 BNF/Coinduction.thy ~> Coinduction.thy |
|
74 BNF/More_BNFs.thy ~> Library/More_BNFs.thy |
|
75 BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy |
|
76 BNF/Examples/* ~> BNF_Examples/* |
|
77 New theories: |
|
78 List_Prefix.thy (split from Library/Sublist.thy) |
|
79 Wellorder_Extension.thy (split from Zorn.thy) |
|
80 Library/Cardinal_Notations.thy |
|
81 Library/BNF_Decl.thy |
|
82 BNF_Examples/Misc_Primcorec.thy |
|
83 BNF_Examples/Stream_Processor.thy |
|
84 Discontinued theory: |
|
85 BNF/BNF.thy |
|
86 BNF/Equiv_Relations_More.thy |
|
87 |
|
88 * New theory: |
|
89 Cardinals/Ordinal_Arithmetic.thy |
|
90 |
|
91 * Theory reorganizations: |
|
92 * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy |
48 |
93 |
49 * The symbol "\<newline>" may be used within char or string literals |
94 * The symbol "\<newline>" may be used within char or string literals |
50 to represent (Char Nibble0 NibbleA), i.e. ASCII newline. |
95 to represent (Char Nibble0 NibbleA), i.e. ASCII newline. |
51 |
96 |
52 * Activation of Z3 now works via "z3_non_commercial" system option |
97 * Activation of Z3 now works via "z3_non_commercial" system option |