src/HOL/HoareParallel/ROOT.ML
author schirmer
Thu, 06 Nov 2003 20:45:02 +0100
changeset 14255 e6e3e3f0deed
parent 13020 791e3b4c4039
child 24104 719fbe4fb77f
permissions -rw-r--r--
Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
time_use_thy "OG_Examples";
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     3
time_use_thy "Gar_Coll";
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     4
time_use_thy "Mul_Gar_Coll";
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     5
time_use_thy "RG_Examples";