2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-21 wenzelm 2000-05-21 added sort_of_term; export sortT;
2000-05-21 wenzelm 2000-05-21 added read_sort;
2000-05-21 wenzelm 2000-05-21 *** empty log message ***
2000-05-21 wenzelm 2000-05-21 new stuff;
2000-05-21 wenzelm 2000-05-21 \urlstyle{rm};
2000-05-21 wenzelm 2000-05-21 snapshot of new Isar'ized version;
2000-05-20 nipkow 2000-05-20 added lemma.
2000-05-20 nipkow 2000-05-20 fixed link
2000-05-18 wenzelm 2000-05-18 * HOL/ML: even fewer consts are declared as global (see theories Ord, Lfp, Gfp, WF); this only affects ML packages that refer to const names internally; * 'pr' command: no longer prints theory contexts, but only proof states;
2000-05-18 wenzelm 2000-05-18 print_state: flag for proof only;
2000-05-18 wenzelm 2000-05-18 hide: check declared;
2000-05-18 wenzelm 2000-05-18 added disable_pr, enable_pr;
2000-05-18 wenzelm 2000-05-18 'pr' now prints actual proof states only;
2000-05-18 wenzelm 2000-05-18 fewer consts declared as global;
2000-05-18 wenzelm 2000-05-18 'apply' consumes facts;
2000-05-17 wenzelm 2000-05-17 Proof General -- if present make this the default;
2000-05-17 wenzelm 2000-05-17 export generic_simp_tac;
2000-05-16 paulson 2000-05-16 changed to cope with the rewriting of #2+n to Suc(Suc n)
2000-05-16 paulson 2000-05-16 new policy to simplify the use of numerals: #0 -> 0 #1 -> 1 #2 + n -> Suc (Suc n) similarly for n + #2
2000-05-16 paulson 2000-05-16 reverted to old proof of dominoes_tile_row, given new treatment of #2+...
2000-05-15 berghofe 2000-05-15 Replaced some definitions involving epsilon by more readable primrec definitions.
2000-05-15 berghofe 2000-05-15 alist_rec and assoc are now defined using primrec and thus no longer refer to the recursion combinator list_rec, which should be considered internal.
2000-05-15 berghofe 2000-05-15 Removed unnecessary primrec equations of hd and last involving arbitrary.
2000-05-15 paulson 2000-05-15 collected three proofs into rename_client_map_tac
2000-05-15 paulson 2000-05-15 added the dummy theory Integ/NatSimprocs.thy
2000-05-12 paulson 2000-05-12 updated
2000-05-12 paulson 2000-05-12 new simprules needed because of new subtraction rewriting
2000-05-12 paulson 2000-05-12 nat_diff_split' now called nat_diff_split
2000-05-12 paulson 2000-05-12 deleted a lot of obsolete arithmetic lemmas
2000-05-12 paulson 2000-05-12 tidied
2000-05-12 paulson 2000-05-12 new simprules for nat_case and nat_rec simplify_meta_eq now maps #0 to 0 and #1 to 1 in its result
2000-05-12 paulson 2000-05-12 tidying, especially to remove zcompare_rls from proofs
2000-05-12 paulson 2000-05-12 a massive tidy-up
2000-05-12 paulson 2000-05-12 NatSimprocs is now a theory, not a file
2000-05-12 paulson 2000-05-12 new theorem one_le_power
2000-05-12 paulson 2000-05-12 tidied
2000-05-12 paulson 2000-05-12 deleted some redundant simprules Added new simprules for subtraction
2000-05-12 paulson 2000-05-12 new dummy theory; prevents strange errors when loading NatSimprocs.ML
2000-05-12 wenzelm 2000-05-12 improved name of simproc;
2000-05-10 wenzelm 2000-05-10 fixed theory deps;
2000-05-10 wenzelm 2000-05-10 base on IntArith instead of Int (in order to leave out deleted simproc!);
2000-05-10 wenzelm 2000-05-10 dest_mss: sort procs wrt. names;
2000-05-10 wenzelm 2000-05-10 FAKE_BUILD;
2000-05-10 wenzelm 2000-05-10 polyml;
2000-05-10 wenzelm 2000-05-10 tuned;
2000-05-10 paulson 2000-05-10 new default simprule for better compatibility with old setup
2000-05-10 paulson 2000-05-10 tidied
2000-05-10 wenzelm 2000-05-10 tuned;
2000-05-09 wenzelm 2000-05-09 use proper version of pdfsetup.sty;
2000-05-09 wenzelm 2000-05-09 added semicolons;
2000-05-09 wenzelm 2000-05-09 updated keywords;
2000-05-09 wenzelm 2000-05-09 named "op ^" definitions;
2000-05-09 wenzelm 2000-05-09 improved X-Symbol stuff;
2000-05-09 paulson 2000-05-09 more examples
2000-05-08 wenzelm 2000-05-08 added INSTALL;
2000-05-08 wenzelm 2000-05-08 moved theory Sexp to Induct examples;
2000-05-08 wenzelm 2000-05-08 strip = impI allI allI;
2000-05-08 wenzelm 2000-05-08 replaced rabs by overloaded abs;
2000-05-08 paulson 2000-05-08 yet another example