--- a/Admin/isatest/settings/at-poly Tue Apr 03 20:56:32 2012 +0200
+++ b/Admin/isatest/settings/at-poly Tue Apr 03 21:09:09 2012 +0200
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.3.0"
- ML_SYSTEM="polyml-5.3.0"
+ POLYML_HOME="/home/polyml/polyml-5.2.1"
+ ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/Admin/isatest/settings/at-poly-e Tue Apr 03 20:56:32 2012 +0200
+++ b/Admin/isatest/settings/at-poly-e Tue Apr 03 21:09:09 2012 +0200
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/doc-src/Dirs Tue Apr 03 20:56:32 2012 +0200
+++ b/doc-src/Dirs Tue Apr 03 21:09:09 2012 +0200
@@ -1,1 +1,1 @@
-Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer
+Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer ProgProve
--- a/doc-src/ProgProve/IsaMakefile Tue Apr 03 20:56:32 2012 +0200
+++ b/doc-src/ProgProve/IsaMakefile Tue Apr 03 21:09:09 2012 +0200
@@ -20,7 +20,15 @@
HOL-ProgProve: $(LOG)/HOL-ProgProve.gz
-$(LOG)/HOL-ProgProve.gz: Thys/*.thy Thys/ROOT.ML
+$(LOG)/HOL-ProgProve.gz: \
+ Thys/Basics.thy \
+ Thys/Bool_nat_list.thy \
+ Thys/Isar.thy \
+ Thys/LaTeXsugar.thy \
+ Thys/Logic.thy \
+ Thys/MyList.thy \
+ Thys/Types_and_funs.thy \
+ Thys/ROOT.ML
@$(USEDIR) -s ProgProve HOL Thys
@rm -f Thys/document/MyList.tex
@rm -f Thys/document/isabelle.sty
--- a/doc/Contents Tue Apr 03 20:56:32 2012 +0200
+++ b/doc/Contents Tue Apr 03 21:09:09 2012 +0200
@@ -1,6 +1,6 @@
Miscellaneous tutorials
tutorial Tutorial on Isabelle/HOL
- main What's in Main
+ prog-prove Programming and Proving in Isabelle/HOL
isar-overview Tutorial on Isar
locales Tutorial on Locales
classes Tutorial on Type Classes
@@ -10,7 +10,8 @@
sledgehammer User's Guide to Sledgehammer
sugar LaTeX Sugar for Isabelle documents
-Main Reference Manuals
+Reference Manuals
+ main What's in Main
isar-ref The Isabelle/Isar Reference Manual
implementation The Isabelle/Isar Implementation Manual
system The Isabelle System Manual
--- a/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 20:56:32 2012 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 21:09:09 2012 +0200
@@ -14,9 +14,9 @@
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
and one :: "'a"
and inverse :: "'a => 'a"
- assumes assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
- and left_one: "\<And>x. one ** x = x"
- and left_inverse: "\<And>x. inverse x ** x = one"
+ assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+ and left_one: "one ** x = x"
+ and left_inverse: "inverse x ** x = one"
begin
text {* some consequences *}
--- a/src/Pure/Isar/bundle.ML Tue Apr 03 20:56:32 2012 +0200
+++ b/src/Pure/Isar/bundle.ML Tue Apr 03 21:09:09 2012 +0200
@@ -91,10 +91,16 @@
let val decls = maps (the_bundle ctxt o prep ctxt) args
in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
-fun gen_context prep_bundle prep_stmt raw_incls raw_elems gthy =
+fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy =
let
val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
- val augment = gen_includes prep_bundle raw_incls #> prep_stmt raw_elems [] #> snd;
+ fun augment ctxt =
+ let
+ val ((_, _, _, ctxt'), _) = ctxt
+ |> Context_Position.restore_visible lthy
+ |> gen_includes prep_bundle raw_incls
+ |> prep_decl ([], []) I raw_elems;
+ in ctxt' |> Context_Position.restore_visible ctxt end;
in
(case gthy of
Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
@@ -115,8 +121,8 @@
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
-val context = gen_context (K I) Expression.cert_statement;
-val context_cmd = gen_context check Expression.read_statement;
+val context = gen_context (K I) Expression.cert_declaration;
+val context_cmd = gen_context check Expression.read_declaration;
end;
--- a/src/Pure/Isar/class_declaration.ML Tue Apr 03 20:56:32 2012 +0200
+++ b/src/Pure/Isar/class_declaration.ML Tue Apr 03 21:09:09 2012 +0200
@@ -157,7 +157,7 @@
fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
#> Class.redeclare_operations thy sups
#> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
- val ((raw_supparams, _, raw_inferred_elems), _) =
+ val ((raw_supparams, _, raw_inferred_elems, _), _) =
Proof_Context.init_global thy
|> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate))
|> prep_decl raw_supexpr init_class_body raw_elems;
@@ -221,7 +221,7 @@
(* process elements as class specification *)
val class_ctxt = Class.begin sups base_sort thy_ctxt;
- val ((_, _, syntax_elems), _) = class_ctxt
+ val ((_, _, syntax_elems, _), _) = class_ctxt
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs =
if null vs then
--- a/src/Pure/Isar/expression.ML Tue Apr 03 20:56:32 2012 +0200
+++ b/src/Pure/Isar/expression.ML Tue Apr 03 21:09:09 2012 +0200
@@ -21,14 +21,14 @@
(* Declaring locales *)
val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
- * Element.context_i list) * ((string * typ) list * Proof.context)
+ * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
- * Element.context_i list) * ((string * typ) list * Proof.context)
+ * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
(*FIXME*)
val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
- * Element.context_i list) * ((string * typ) list * Proof.context)
+ * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
val add_locale: (local_theory -> local_theory) -> binding -> binding ->
expression_i -> Element.context_i list -> theory -> string * local_theory
val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
@@ -357,17 +357,19 @@
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
val inst'' = map2 Type.constraint parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
- val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
+ val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
in (i + 1, insts', ctxt'') end;
- fun prep_elem insts raw_elem (elems, ctxt) =
+ fun prep_elem insts raw_elem ctxt =
let
- val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
- val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
- val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
+ val ctxt' = ctxt
+ |> Context_Position.set_visible false
+ |> declare_elem prep_vars_elem raw_elem
+ |> Context_Position.restore_visible ctxt;
+ val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
in (elems', ctxt') end;
fun prep_concl raw_concl (insts, elems, ctxt) =
@@ -388,7 +390,7 @@
commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
val ctxt4 = init_body ctxt3;
- val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
+ val (elems, ctxt5) = fold_map (prep_elem insts') raw_elems ctxt4;
val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
@@ -458,10 +460,10 @@
val context' = context |>
fix_params fixed |>
fold (Context.proof_map o Locale.activate_facts NONE) deps;
- val (elems', _) = context' |>
+ val (elems', context'') = context' |>
Proof_Context.set_stmt true |>
fold_map activate elems;
- in ((fixed, deps, elems'), (parms, ctxt')) end;
+ in ((fixed, deps, elems', context''), (parms, ctxt')) end;
in
@@ -735,7 +737,7 @@
val _ = Locale.defined thy name andalso
error ("Duplicate definition of locale " ^ quote name);
- val ((fixed, deps, body_elems), (parms, ctxt')) =
+ val ((fixed, deps, body_elems, _), (parms, ctxt')) =
prep_decl raw_import I raw_body (Proof_Context.init_global thy);
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
--- a/src/Pure/Isar/generic_target.ML Tue Apr 03 20:56:32 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML Tue Apr 03 21:09:09 2012 +0200
@@ -121,7 +121,7 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
- val asms' = map (Raw_Simplifier.rewrite_rule defs) asms;
+ val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
(*export fixes*)
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);